search

agda / cubical

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

Some recursive Fin functions #1077

Closed dolio closed 9 months ago

dolio commented 9 months ago

Adds Fin to ℕ and a generalized version of ℕ to Fin (using _<_ rather than just successor).

I found myself needing these when using these as variables in well-scoped lambda terms.

mortberg commented 9 months ago

Looks good to me, but why use the recursive Fin instead of the one in Fin.Base?

dolio commented 9 months ago

I find the recursive Fin better to use in most situations. The other one uses k + m = n ordering, and with cubical paths, this does nothing to rule out impossible pattern matching cases.

mortberg commented 9 months ago

I find the recursive Fin better to use in most situations. The other one uses k + m = n ordering, and with cubical paths, this does nothing to rule out impossible pattern matching cases.

Ok, it's a bit unfortunate that we have 3 different Fin's in the library which are in use... It could be nice to have only one and develop all the theory once and for all instead of three times...