]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/contribs/assembly/freescale/freescale_ocaml/matita_nat_exp.ml
branch for universe
[helm.git] / matita / contribs / assembly / freescale / freescale_ocaml / matita_nat_exp.ml
diff --git a/matita/contribs/assembly/freescale/freescale_ocaml/matita_nat_exp.ml b/matita/contribs/assembly/freescale/freescale_ocaml/matita_nat_exp.ml
new file mode 100644 (file)
index 0000000..dd2b495
--- /dev/null
@@ -0,0 +1,9 @@
+let exp =
+let rec exp = 
+(function n -> (function m -> 
+(match m with 
+   Matita_nat_nat.O -> (Matita_nat_nat.S(Matita_nat_nat.O))
+ | Matita_nat_nat.S(p) -> (Matita_nat_times.times n (exp n p)))
+)) in exp
+;;
+