aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/Cases-bug3758.v
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.