I'm using Emacs with agda-mode, and have written this function:
pow : Nat → Nat → Nat
pow m n = pow' 1 m n
where
pow' : Nat → Nat → Nat → Nat
pow' acc _ zero = acc
pow' acc m (succ n) = pow' (m * acc) m n
Nat, succ and * are defined to be compatible with Agda's internal definitions of natural numbers.
When I evaluate (pow 2 100000) I get a stack overflow error. However, given that the recursive call is a tail call, I would like the agda interpreter to optimize pow' into a loop.
How can I enable this optimization?