|
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.
¤ Dauer der Verarbeitung: 0.13 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.
|
