[Agda] sym in Agda 2.5.1

[Andrés Sicard-Ramírez]

On 14 February 2016 at 02:03, John Leo <leo at halfaya.org> wrote:
> n+0=n : (n : ℕ) → n + 0 ≡ n
> n+0=n zero    = refl
> n+0=n (suc n) = cong suc (n+0=n (n))
>
> m+Sn : (m n : ℕ) → m + suc n ≡ suc (m + n)
> m+Sn zero    n = refl
> m+Sn (suc m) n = cong suc (m+Sn m n)
>
> +comm : (m n : ℕ) → m + n ≡ n + m
> +comm zero    n =
>   let a = sym (n+0=n n)
>   in {!!}
> +comm (suc m) n =
>   let a = cong suc (+comm m n)
>       b = sym (m+Sn n m)
>   in {!!}

Please add which modules are you importing.


-- 
Andrés