search

UniMath / agda-unimath

The agda-unimath library
https://unimath.github.io/agda-unimath/
MIT License
219 stars 70 forks source link

Experiment: both type arguments of const implicit #1097

Closed EgbertRijke closed 6 months ago

EgbertRijke commented 6 months ago

Testing out whether it is feasible to make both type arguments in const can be made implicit.

This PR is not to be merged. Its purpose is merely to facilitate a discussion about changes that were proposed in #1096.