blob: 6e4b20031b1feb8ee941de55eb948a6c261693c7 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
Inductive List (A : Set) : Set :=
| Nil : List A
| Cons : A -> List A -> List A.
Inductive Empty (A : Set) : List A -> Prop :=
intro_Empty : Empty A (Nil A).
Parameter
inv_Empty : forall (A : Set) (a : A) (x : List A), ~ Empty A (Cons A a x).
Type
(fun (A : Set) (l : List A) =>
match l return (Empty A l \/ ~ Empty A l) with
| Nil => or_introl (~ Empty A (Nil A)) (intro_Empty A)
| Cons a y as b => or_intror (Empty A b) (inv_Empty A a y)
end).
|
