matita/contribs/assembly/freescale/freescale_ocaml/matita_nat_primes.ml

   1 let divides_b =
   2 (function n -> (function m -> (Matita_nat_compare.eqb (Matita_nat_div_and_mod.mod_ m n) Matita_nat_nat.O)))
   3 ;;
   4
   5 let smallest_factor =
   6 (function n ->
   7 (match n with
   8    Matita_nat_nat.O -> Matita_nat_nat.O
   9  | Matita_nat_nat.S(p) ->
  10 (match p with
  11    Matita_nat_nat.O -> (Matita_nat_nat.S(Matita_nat_nat.O))
  12  | 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))))
  13 )
  14 )
  15 ;;
  16
  17 let primeb =
  18 (function n ->
  19 (match n with
  20    Matita_nat_nat.O -> Matita_datatypes_bool.False
  21  | Matita_nat_nat.S(p) ->
  22 (match p with
  23    Matita_nat_nat.O -> Matita_datatypes_bool.False
  24  | 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))))))
  25 )
  26 )
  27 ;;
  28