blob: 782b27ce968e045ba524a35c26e37ccce4b6b2b4 (
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
|
Require Extraction.
Extraction Language OCaml.
Set Extraction KeepSingleton.
Module Case1.
Record rec (x : bool) := { f : bool }.
Definition silly x (b : rec x) :=
if x return (if x then bool else unit) then f x b else tt.
End Case1.
Module Case2.
Record rec (x : bool) := { f : bool -> bool }.
Definition silly x (b : rec x) :=
if x return (if x then bool else unit) then f x b false else tt.
End Case2.
Extraction TestCompile Case1.silly Case2.silly.
Recursive Extraction Case1.silly Case2.silly.
|
