blob: 31eafc36e1a74c63229d63cf193c27fbe68eca44 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
|
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).
|
