diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2015-09-03 19:37:22 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2015-09-03 19:37:22 +0200 |
| commit | b5c646a37ac0375f9fbb2427549c925ee3f127ad (patch) | |
| tree | 4a4159636206bce92eab5e89a0cb71aecac21cc8 /plugins/extraction/ExtrHaskellNatNum.v | |
| parent | 5c060d56a9d94d74cdeca6f6b424306218e81562 (diff) | |
Improve directives for Haskell extraction of nat.
Diffstat (limited to 'plugins/extraction/ExtrHaskellNatNum.v')
| -rw-r--r-- | plugins/extraction/ExtrHaskellNatNum.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/plugins/extraction/ExtrHaskellNatNum.v b/plugins/extraction/ExtrHaskellNatNum.v index 81d76a5ff..244eb85fc 100644 --- a/plugins/extraction/ExtrHaskellNatNum.v +++ b/plugins/extraction/ExtrHaskellNatNum.v @@ -15,6 +15,8 @@ Extract Inlined Constant Nat.max => "Prelude.max". Extract Inlined Constant Nat.min => "Prelude.min". Extract Inlined Constant Init.Nat.add => "(Prelude.+)". Extract Inlined Constant Init.Nat.mul => "(Prelude.*)". +Extract Inlined Constant Init.Nat.max => "Prelude.max". +Extract Inlined Constant Init.Nat.min => "Prelude.min". Extract Inlined Constant Compare_dec.lt_dec => "(Prelude.<)". Extract Inlined Constant Compare_dec.leb => "(Prelude.<=)". Extract Inlined Constant Compare_dec.le_lt_dec => "(Prelude.<=)". @@ -24,6 +26,10 @@ Extract Inlined Constant Peano_dec.eq_nat_dec => "(Prelude.==)". Extract Constant Nat.pred => "(\n -> Prelude.max 0 (Prelude.pred n))". Extract Constant Nat.sub => "(\n m -> Prelude.max 0 (n Prelude.- m))". +Extract Constant Init.Nat.pred => "(\n -> Prelude.max 0 (Prelude.pred n))". +Extract Constant Init.Nat.sub => "(\n m -> Prelude.max 0 (n Prelude.- m))". Extract Constant Nat.div => "(\n m -> if m Prelude.== 0 then 0 else Prelude.div n m)". Extract Constant Nat.modulo => "(\n m -> if m Prelude.== 0 then 0 else Prelude.mod n m)". +Extract Constant Init.Nat.div => "(\n m -> if m Prelude.== 0 then 0 else Prelude.div n m)". +Extract Constant Init.Nat.modulo => "(\n m -> if m Prelude.== 0 then 0 else Prelude.mod n m)".
\ No newline at end of file |