Hi all,
Coq has the nice Numeral Notation feature, which is a uniform way how to declare notations for number-like data types (like nat, 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.)
Thanks
Maximilian
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 lia.
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.