This does not get us builtin syntax for constructing finite numbers, which would be nice to have and easy to do with a builtin fin.
The problem is mainly implementing eliminators for the builtin, but perhaps the userland version can be a guide for how to do so.
We would also want coercions between fin and nat and those get tricky, especially if we don't have all of the laws on natural numbers as definitional equalities.
For how a user-defined fin works, see https://github.com/ToposInstitute/polytt/blob/poly-cont/examples/fin.poly. It is missing some definitional equalities so it doesn't quite have a proper induction statement, but it is close (modulo some rewriting across propositional equalities).
This does not get us builtin syntax for constructing finite numbers, which would be nice to have and easy to do with a builtin fin.
The problem is mainly implementing eliminators for the builtin, but perhaps the userland version can be a guide for how to do so.
We would also want coercions between fin and nat and those get tricky, especially if we don't have all of the laws on natural numbers as definitional equalities.