Skip to content

Builtin CONS no longer exists #7

@bblfish

Description

@bblfish

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.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions