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
57
58
59
60
|
From Coq Require Extraction.
Record mixin_of T0 (b : unit) (T := T0) := Mixin { _ : T0 -> let U:=T0 in U }.
Definition d := Mixin nat tt (fun x => x).
Extraction TestCompile d.
(* Extra tests *)
Record R T0 (b:nat) (c:=b) (T:=T0) (e:nat) (d:c=e) := Build
{ g : T0 -> let U:=T0 in U ; h : d = d ; x : nat ; y := x+x }.
Definition r := {| g := (fun x : nat => x) ; h := eq_refl (eq_refl 0) ; x := 0 |}.
Extraction TestCompile r.
(*
(** val r0 : nat r **)
let r0 =
{ g = (fun x0 -> x0); x = O }
*)
Inductive I T (a:T) (U:=T) (b:T) (c:=(a,b)) : forall d (e:=S d) (h : S d = e), Type :=
| C : I T a b 0 eq_refl
| D : J T a b true eq_refl -> I T a b 1 eq_refl
with J T (a:T) (U:=T) (b:T) (c:=(a,b)) : forall (d:bool) (h:d = true), Type :=
| E : I T a b 0 eq_refl -> J T a b true eq_refl.
Definition c := D _ _ _ (E _ _ _ (C nat 0 0)).
Extraction TestCompile c.
(*
(** val c : nat i **)
let c =
D (E C)
*)
CoInductive V T0 (b:nat) (c:=b) (T:=T0) (e:nat) (d:c=e) :=
{ k : T; b := c+e ; m : nat; z : option (W nat 0 0 eq_refl) }
with W T0 (b:nat) (c:=b) (T:=T0) (e:nat) (d:c=e) :=
{ l : V nat 0 0 eq_refl }.
CoFixpoint v :=
{| k := 0 ; m := 0 ; z := Some w ; |}
with w := {| l := v |}.
Extraction TestCompile v.
(*
(** val v0 : nat v **)
let rec v0 =
lazy (Build_V (O, O, (Some w0)))
(** val w0 : nat w **)
and w0 =
lazy (Build_W v0)
*)
|
