blob: 25d78f4b0e6283eb5d23009bfced46d682c2bb5a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
(* Computing the type constraints to be satisfied when building the
return clause of a match with a match *)
Set Implicit Arguments.
Set Asymmetric Patterns.
Variable A : Type.
Variable typ : A -> Type.
Inductive t : list A -> Type :=
| snil : t nil
| scons : forall (x : A) (e : typ x) (lx : list A) (le : t lx), t (x::lx).
Definition car (x:A) (lx : list A) (s: t (x::lx)) : typ x :=
match s in t l' with
| snil => False
| scons _ e _ _ => e
end.
|
