branch for universe

[helm.git] / matita / contribs / assembly / freescale / freescale_ocaml / matita_nat_minus.ml

diff --git a/matita/contribs/assembly/freescale/freescale_ocaml/matita_nat_minus.ml b/matita/contribs/assembly/freescale/freescale_ocaml/matita_nat_minus.ml
new file mode 100644 (file)
index 0000000..b309f29
--- /dev/null
+++ b/matita/contribs/assembly/freescale/freescale_ocaml/matita_nat_minus.ml
@@ -0,0 +1,13 @@
+let minus =
+let rec minus = 
+(function n -> (function m -> 
+(match n with 
+   Matita_nat_nat.O -> Matita_nat_nat.O
+ | Matita_nat_nat.S(p) -> 
+(match m with 
+   Matita_nat_nat.O -> (Matita_nat_nat.S(p))
+ | Matita_nat_nat.S(q) -> (minus p q))
+)
+)) in minus
+;;
+