search

agda / cubical

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

Supply implicit argument for agda/agda#7390 #1143

Closed andreasabel closed 3 months ago

andreasabel commented 3 months ago

This small change makes the code more robust w.r.t. the Agda type checker, in particular enabling Agda PR #7349 #7390.

felixwellen commented 3 months ago

Is this the right PR? https://github.com/agda/agda/pull/7349

andreasabel commented 3 months ago

No, sorry, agda/agda#7390

felixwellen commented 3 months ago

It is certainly good to get rid of this hack, so I'll merge this.

andreasabel commented 3 months ago

Thanks!