|
(* @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.
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
