OCaml extraction: driver for mach.peano.Peano

parent c75a21ca
......@@ -222,6 +222,30 @@ module mach.int.Int63
syntax val of_bv "(fun x -> x)"*)
end
module mach.peano.Peano
syntax type t "int"
syntax val to_int "Z.of_int %1"
syntax val of_int "Z.to_int %1"
syntax val zero "0"
syntax val succ "%1 + 1"
syntax val pred "%1 - 1"
syntax val lt "%1 < %2"
syntax val le "%1 <= %2"
syntax val gt "%1 > %2"
syntax val ge "%1 >= %2"
syntax val eq "%1 = %2"
syntax val ne "%1 <> %2"
syntax val neg "- %1"
syntax val abs "abs %1"
syntax val add "%1 + %2"
syntax val sub "%1 - %2"
syntax val mul "%1 * %2"
syntax val div "%1 / %2"
syntax val mod "%1 mod %2"
syntax val max "max %1 %2"
syntax val min "min %1 %2"
end
module mach.onetime.OneTime
syntax type t "int"
syntax val to_int "Z.of_int %1"
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment