blob: e48f452326d14ce17b2c140235631bd9b817490d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
(* There used to be an evar leak in the to_nat example *)
Require Import Coq.Lists.List.
Import ListNotations.
Fixpoint Idx {A:Type} (l:list A) : Type :=
match l with
| [] => False
| _::l => True + Idx l
end.
Fixpoint to_nat {A:Type} (l:list A) (i:Idx l) : nat :=
match l,i with
| [] , i => match i with end
| _::_, inl _ => 0
| _::l, inr i => S (to_nat l i)
end.
|
