diff options
Diffstat (limited to 'test-suite')
-rw-r--r-- | test-suite/output/Extraction_infix.out | 16 | ||||
-rw-r--r-- | test-suite/output/Extraction_infix.v | 21 |
2 files changed, 37 insertions, 0 deletions
diff --git a/test-suite/output/Extraction_infix.out b/test-suite/output/Extraction_infix.out new file mode 100644 index 000000000..35ded8013 --- /dev/null +++ b/test-suite/output/Extraction_infix.out @@ -0,0 +1,16 @@ +(** val test : foo **) + +let test = + (fun (b, p) -> bar) (True, False) +(** val test : foo **) + +let test = + True@@?False +(** val test : foo **) + +let test = + True#^^False +(** val test : foo **) + +let test = + True@?:::False diff --git a/test-suite/output/Extraction_infix.v b/test-suite/output/Extraction_infix.v new file mode 100644 index 000000000..bc0ddb3e1 --- /dev/null +++ b/test-suite/output/Extraction_infix.v @@ -0,0 +1,21 @@ +(* @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. |