[Agda] sharing a variable in a with clause and its result

[Kenichi Asai]

Suppose we have a function like this (Agda source attached):

f : (m n : N) -> N
f zero n = n
f (suc m) n with f m (suc n)
... | x = x + suc n

Can I introduce a shared variable and name the common subexpression
"suc n"?  Using a where clause, I can abstract the second "suc n" as
follows, but not the first one:

g : (m n : N) -> N
g zero n = n
g (suc m) n with g m (suc n)
... | x = x + n'
  where n' = suc n

Using a let clause, I can abstract the first one but not the second
one:

h : (m n : N) -> N
h zero n = n
h (suc m) n with let n' = suc n in h m n'
... | x = x + suc n

I can think of introducing a helper function, but would that be the
only option?  Thanks in advance!

Sincerely,

-- 
Kenichi Asai
-------------- next part --------------
module a where

open import Data.Nat

f : (m n : ?) ? ?
f zero n = n
f (suc m) n with f m (suc n)
... | x = x + suc n

g : (m n : ?) ? ?
g zero n = n
g (suc m) n with g m (suc n)
... | x = x + n'
  where n' = suc n

h : (m n : ?) ? ?
h zero n = n
h (suc m) n with let n' = suc n in h m n'
... | x = x + suc n