Closed claymager closed 2 years ago
Thanks for this! Could you update the idris2 submodule to latest please?
I think I did that right? I haven't actually used submodules before.
Ah. See idris-lang/idris2#2134:
Currently, sourcedir = "."
is broken.
Inigo.ipkg
is generated, you should change Inigo.dhall
instead. Ideally that file should be added to .gitignore
.
Prelude now sets Eq and Show to be total by default, so we need to mark them as covering in order to build.