diff options
Diffstat (limited to 'plugins/micromega/MExtraction.v')
| -rw-r--r-- | plugins/micromega/MExtraction.v | 20 |
1 files changed, 19 insertions, 1 deletions
diff --git a/plugins/micromega/MExtraction.v b/plugins/micromega/MExtraction.v index a5ac92db86..b4b40ca733 100644 --- a/plugins/micromega/MExtraction.v +++ b/plugins/micromega/MExtraction.v @@ -20,4 +20,22 @@ Require Import VarMap. Require Import RingMicromega. Require Import NArith. -Extraction "micromega.ml" List.map simpl_cone map_cone indexes n_of_Z Nnat.N_of_nat ZTautoChecker QTautoChecker find. +Extract Inductive prod => "( * )" [ "(,)" ]. +Extract Inductive List.list => list [ "[]" "(::)" ]. +Extract Inductive bool => bool [ true false ]. +Extract Inductive sumbool => bool [ true false ]. +Extract Inductive option => option [ Some None ]. +Extract Inductive sumor => option [ Some None ]. +(** Then, in a ternary alternative { }+{ }+{ }, + - leftmost choice (Inleft Left) is (Some true), + - middle choice (Inleft Right) is (Some false), + - rightmost choice (Inright) is (None) *) + + +(** To preserve its laziness, andb is normally expansed. + Let's rather use the ocaml && *) +Extract Inlined Constant andb => "(&&)". + +Extraction "micromega.ml" + List.map simpl_cone map_cone indexes + n_of_Z Nnat.N_of_nat ZTautoChecker QTautoChecker find. |