branch for universe

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

diff --git a/matita/contribs/assembly/freescale/freescale_ocaml/matita_nat_sigma_and_pi.ml b/matita/contribs/assembly/freescale/freescale_ocaml/matita_nat_sigma_and_pi.ml
new file mode 100644 (file)
index 0000000..46c043f
--- /dev/null
+++ b/matita/contribs/assembly/freescale/freescale_ocaml/matita_nat_sigma_and_pi.ml
@@ -0,0 +1,18 @@
+let sigma =
+let rec sigma = 
+(function n -> (function f -> (function m -> 
+(match n with 
+   Matita_nat_nat.O -> (f m)
+ | Matita_nat_nat.S(p) -> (Matita_nat_plus.plus (f (Matita_nat_plus.plus (Matita_nat_nat.S(p)) m)) (sigma p f m)))
+))) in sigma
+;;
+
+let pi =
+let rec pi = 
+(function n -> (function f -> (function m -> 
+(match n with 
+   Matita_nat_nat.O -> (f m)
+ | Matita_nat_nat.S(p) -> (Matita_nat_times.times (f (Matita_nat_plus.plus (Matita_nat_nat.S(p)) m)) (pi p f m)))
+))) in pi
+;;
+