Closed Z-snails closed 3 years ago
Due to various changes to idris2, there were some errors, which I have fixed.
do
ignore
"""
.ipkg
some
List1
forget
Draft, because other changes are still causing problems.
Due to various changes to idris2, there were some errors, which I have fixed.
do
notation no longer silently discards values, so addedignore
"""
and have more newlines.ipkg
files is now usedsome
returnsList1
, so addedforget