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

[Nils Anders Danielsson]

On 2016-01-03 04:11, Kenichi Asai wrote:
> 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

Here's another option:

   i : (m n : ℕ) → ℕ
   i zero n = n
   i (suc m) n with n' | h m n'
     where n' = suc n
   ... | n' | x = x + n'

-- 
/NAD