[Agda] simple question
Andreas Abel
andreas.abel at ifi.lmu.de
Tue Oct 14 10:01:40 CEST 2014
Besides the point that induction is not needed and a simple
eq-succ (refl _) = refl _
suffices, the error you get stems from the fact that you confused proof
and proposition in the induction step. You write the proposition
((succ i) + m) == (plus (succ i) m)
where you should have written a /proof/ of this proposition.
Cheers,
Andreas
On 14.10.2014 04:13, Andrew Harris wrote:
> Hello,
>
> I'm trying to follow along in the very good paper "Dependent Types
> At Work" written by Ana Bove and Peter Dybjer. I'm stuck at trying to
> prove "eq-succ", which is one of the exercises in Section 4.4. The
> closest I can make it is the following:
>
> {- proof of eq-succ -}
> eq-succ : {n m : Nat} → n == m → succ n == succ m
> eq-succ (refl m) = natrec {(\k → (k + m) == (plus k m))} (refl m) (\i h
> → ((succ i) + m) == (plus (succ i) m)) m
>
> But this does not typecheck, I get the error:
>
> Set !=< (succ i + m) == plus (succ i) m of type Set₁
> when checking that the expression (succ i + m) == plus (succ i) m
> has type (succ i + m) == plus (succ i) m
>
> I'm stuck -- I don't quite understand what I'm supposed to create an
> element of Set_1 that has a signature of (succ i + m) == plus (succ i)
> m, (if that's what I'm supposed to do). Any hints would be appreciated!
>
> -andrew
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
--
Andreas Abel <>< Du bist der geliebte Mensch.
Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden
andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/
More information about the Agda
mailing list