blob: 2f06ad39721cad2382ba7f9ee1061e70ddfb465b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
|
Extraction nat.
Extraction [x:nat]x.
Inductive c [x:nat] : nat -> Set :=
refl : (c x x)
| trans : (y,z:nat)(c x y)->(le y z)->(c x z).
Extraction c.
Extraction [f:nat->nat][x:nat](f x).
Extraction [f:nat->Set->nat][x:nat](f x nat).
Extraction [f:(nat->nat)->nat][x:nat][g:nat->nat](f g).
Extraction (pair nat nat (S O) O).
Definition f := [x:nat][_:(le x O)](S x).
Extraction (f O (le_n O)).
Extraction ([X:Set][x:X]x nat).
Definition d := [X:Type]X.
Extraction d.
Extraction (d Set).
Extraction [x:(d Set)]O.
Extraction (d nat).
Extraction ([x:(d Type)]O Type).
Extraction ([x:(d Type)]x).
Extraction ([X:Type][x:X]x Set nat).
Definition id' := [X:Type][x:X]x.
Extraction id'.
Extraction (id' Set nat).
Extraction let t = nat in (id' Set t).
Definition Ensemble := [U:Type]U->Prop.
Definition Empty_set := [U:Type][x:U]False.
Definition Add := [U:Type][A:(Ensemble U)][x:U][y:U](A y) \/ x==y.
Inductive Finite [U:Type] : (Ensemble U) -> Set :=
Empty_is_finite: (Finite U (Empty_set U))
| Union_is_finite:
(A: (Ensemble U)) (Finite U A) ->
(x: U) ~ (A x) -> (Finite U (Add U A x)).
Extraction Finite.
Extraction ([X:Type][x:X]O Type Type).
|
