I have a historical question: When did indexed finite types
Inductive fin : nat -> Type := | Zero: forall n, fin (S n) | Succ: forall n, fin n -> fin (S n).
appear first in Coq or elsewhere?
I checked Martin-Löf, but there finite types are obtained with n constructors, not just 2. The above definition appears in Chlipala’s CPDT. I did not find it in Coq’Art.
Related: When did the recursive version with option types appear first?
Fixpoint Fin (n: nat) : Type := match n with | 0 => False | S n' => option (Fin n') end.
Thanks in advance. Gert