search

agda / cubical

An experimental library for Cubical Agda
https://agda.github.io/cubical/Cubical.README.html
Other
441 stars 134 forks source link

Add --guardedness globally and remove Codata.Everything #1139

Open mortberg opened 3 weeks ago

mortberg commented 3 weeks ago

Any objections to this? As far as I understand --guardedness is safe and doesn't interfere with anything, but the Codata folder needs it.

This should allow us to simplify the build process in a future PR as we just need to generate the Everything files without any special treatment for some folders

mortberg commented 3 weeks ago

Ps: me looking into this was prompted by https://github.com/agda/cubical/pull/1129 which would benefit from global --guardedness