agda-lecture-notes icon indicating copy to clipboard operation
agda-lecture-notes copied to clipboard

Published 20 hours ago • verified publisher icon jespercockx

numeral 6 cannot be used yet

Open dimitri-xyz opened this issue 2 years ago • 2 comments

We have not defined 6 with {-# BUILTIN NATURAL } yet. So, Agda is complaining about this. It also makes more sense to me to see this type as IsEven (suc (suc (suc (suc (suc (suc zero)))))) to make the pattern matching on the constructors clear.

https://github.com/jespercockx/agda-lecture-notes/blob/f3c8529504684a275b3cac569bea21b0476c1d3f/agda.lagda.tex#L1576

I am reading the notes as a fully self contained tutorial. My apologies is that is not the intent.

dimitri-xyz avatar Apr 07 '22 07:04 dimitri-xyz

There's a sidenote about literals for natural numbers at https://github.com/jespercockx/agda-lecture-notes/blob/f3c8529504684a275b3cac569bea21b0476c1d3f/agda.lagda.tex#L385-L395, if you include this code then the example should work!

jespercockx avatar Apr 10 '22 09:04 jespercockx

Indeed, it does. As this was a side note, it wasn't clear that the text would assume that the BUILTIN pragma was used after that point.

dimitri-xyz avatar May 16 '22 07:05 dimitri-xyz