Hi
I hope you don't mind me copying this reply to the mailing list, as it
may be of more general interest.
Jonathan Lee wrote:
I've been trying the tutorial and I'm coming to the part about the
(vec x) function. I'm a bit confused on how the implicit syntax as
when I input:
( n : Nat ;
Conor McBride wrote:
I also apologise for the way Mozilla Thunderbird arbitrarily turns my
code into jigsaw puzzles.
I hate computers.
All the best
Conor
Sorry for the code presentation, too.
Perhaps it's better to attach a small piece of code :
The last clause was rejected, (I presume) because of the
non-unification of
(suc n) with (plus n (suc zero)). Is that right ?
Is there a way to use some commutatitivy of plus (like using JMeq in
