Coq has the nice
Numeral Notation feature, which is a uniform way how to declare notations for number-like data types (like
Z, etc.) However, it doesn’t work for
Fin.t, because it is parametrised by a number. This forces one to use an uggly file like this one. Do you know better solutions?
(I don’t want to write an ocaml plugin though; I’m just curious.)
Possible slight improvement: wrap your getFin in
Notation "fin n” := (ltac:(getFin n)) or sth. like that (haven’t tried), use search-n-replace to fix call sites, and remove the boilerplate?
As an alternative implementation to avoid Ltac, and since you use this for constants, I’d maybe define
toFin (m n : nat) (Hle: Nat.ltb m n = true) : Fin n and call it as
Notation “fin m” := (toFin m _ eq_refl).: I’m using the decidable version of less-than to avoid calling
Better error messages can be arranged via Ltac.
I had similar ideas. Both of your ideas, however, only work for parsing.
I wonder whether there’s some real limitation preventing this or if it’s just not implemented yet. Might be worth asking @JasonGross.
I’ve made an issue for this at coq/coq#12035. There are actually two enhancement requests bundled as one in that issue (one to allow numeral notations for type families with a specific, given, concrete parameter, and another to allow numeral notations for type families which are quantified over all possible values of the parameters (though these could in principle be mixed)). The answer, by and large, is that it’s just not implemented yet, and I describe in that issue roughly what it would take to implement it.