CS410-17 icon indicating copy to clipboard operation
CS410-17 copied to clipboard

Builtin CONS no longer exists

Open bblfish opened this issue 4 years ago • 0 comments

Doing exercise 1 I found this warning:

/Volumes/Dev/Programming/Proof/Agda/exercises/CS410-2017/course/exercises/CS410-Prelude.agda:173,1-26
Builtin CONS no longer exists. It is now bound by BUILTIN LIST
when checking the pragma BUILTIN CONS _,-_

/Volumes/Dev/Programming/Proof/Agda/exercises/CS410-2017/course/exercises/CS410-Prelude.agda:172,1-23
Builtin NIL no longer exists. It is now bound by BUILTIN LIST
when checking the pragma BUILTIN NIL []

I'll continue as it is just a warning and try to fix later when I get better.

bblfish avatar Oct 10 '20 15:10 bblfish