search

agda / cubical

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

Clean up: Remove Foundation/Everything and outdated stuff #1127

Closed felixwellen closed 4 months ago

felixwellen commented 4 months ago

Discussed with anders already -> merging.

ncfavier commented 4 months ago

What's the replacement for Cubical.{Core,Foundations}.Everything? The generated files only have import, not open import.

mortberg commented 3 months ago

What's the replacement for Cubical.{Core,Foundations}.Everything? The generated files only have import, not open import.

I think the idea is just to write the imports one needs instead of relying on the Everything files