WIP

Author: andres-erbsen

theories/Vectors/Fin.v

@@ -38,6 +38,12 @@ Inductive t : nat -> Set :=
 |F1 : forall {n}, t (S n)
 |FS : forall {n}, t n -> t (S n).
 
+Fixpoint to_nat' {n} (p : t n) : nat :=
+  match p with
+  | F1 => 0
+  | FS p => S (to_nat' p)
+  end.
+
 Section SCHEMES.
 Definition case0 P (p: t 0): P p :=
   match p with | F1 | FS  _ => fun devil => False_rect (@ID) devil (* subterm !!! *) end.