blob: fe5926a36acd7bc8acd982d17ad709135bfa5aac (
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
|
(* @herbelin's example for issue #6212 *)
Require Import Extraction.
Inductive I := C : bool -> bool -> I.
Definition test := C true false.
(* the parentheses around the function wrong signalled an infix operator *)
Extract Inductive I => "foo" [ "(fun (b, p) -> bar)" ].
Extraction test.
(* some bonafide infix operators *)
Extract Inductive I => "foo" [ "(@@?)" ].
Extraction test.
Extract Inductive I => "foo" [ "(#^^)" ].
Extraction test.
Extract Inductive I => "foo" [ "(@?:::)" ].
Extraction test.
(* allow whitespace around infix operator *)
Extract Inductive I => "foo" [ "( @?::: )" ].
Extraction test.
|
