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.

2 Likes