X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fcontribs%2Fassembly%2Ffreescale%2Ffreescale_ocaml%2Fmatita_nat_primes.ml;fp=matita%2Fcontribs%2Fassembly%2Ffreescale%2Ffreescale_ocaml%2Fmatita_nat_primes.ml;h=894df89044fa5ef29ba0af911a3c15c7503631d2;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1

diff --git a/matita/contribs/assembly/freescale/freescale_ocaml/matita_nat_primes.ml b/matita/contribs/assembly/freescale/freescale_ocaml/matita_nat_primes.ml
new file mode 100644
index 000000000..894df8904
--- /dev/null
+++ b/matita/contribs/assembly/freescale/freescale_ocaml/matita_nat_primes.ml
@@ -0,0 +1,28 @@
+let divides_b =
+(function n -> (function m -> (Matita_nat_compare.eqb (Matita_nat_div_and_mod.mod_ m n) Matita_nat_nat.O)))
+;;
+
+let smallest_factor =
+(function n -> 
+(match n with 
+   Matita_nat_nat.O -> Matita_nat_nat.O
+ | Matita_nat_nat.S(p) -> 
+(match p with 
+   Matita_nat_nat.O -> (Matita_nat_nat.S(Matita_nat_nat.O))
+ | Matita_nat_nat.S(q) -> (Matita_nat_minimization.min_aux q (Matita_nat_nat.S((Matita_nat_nat.S(Matita_nat_nat.O)))) (function m -> (Matita_nat_compare.eqb (Matita_nat_div_and_mod.mod_ (Matita_nat_nat.S((Matita_nat_nat.S(q)))) m) Matita_nat_nat.O))))
+)
+)
+;;
+
+let primeb =
+(function n -> 
+(match n with 
+   Matita_nat_nat.O -> Matita_datatypes_bool.False
+ | Matita_nat_nat.S(p) -> 
+(match p with 
+   Matita_nat_nat.O -> Matita_datatypes_bool.False
+ | Matita_nat_nat.S(q) -> (Matita_nat_compare.eqb (smallest_factor (Matita_nat_nat.S((Matita_nat_nat.S(q))))) (Matita_nat_nat.S((Matita_nat_nat.S(q))))))
+)
+)
+;;
+