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

   1 let mod_aux =
   2 let rec mod_aux =
   3 (function p -> (function m -> (function n ->
   4 (match (Matita_nat_compare.leb m n) with
   5    Matita_datatypes_bool.True -> m
   6  | Matita_datatypes_bool.False ->
   7 (match p with
   8    Matita_nat_nat.O -> m
   9  | Matita_nat_nat.S(q) -> (mod_aux q (Matita_nat_minus.minus m (Matita_nat_nat.S(n))) n))
  10 )
  11 ))) in mod_aux
  12 ;;
  13
  14 let mod_ =
  15 (function n -> (function m ->
  16 (match m with
  17    Matita_nat_nat.O -> n
  18  | Matita_nat_nat.S(p) -> (mod_aux n n p))
  19 ))
  20 ;;
  21
  22 let div_aux =
  23 let rec div_aux =
  24 (function p -> (function m -> (function n ->
  25 (match (Matita_nat_compare.leb m n) with
  26    Matita_datatypes_bool.True -> Matita_nat_nat.O
  27  | Matita_datatypes_bool.False ->
  28 (match p with
  29    Matita_nat_nat.O -> Matita_nat_nat.O
  30  | Matita_nat_nat.S(q) -> (Matita_nat_nat.S((div_aux q (Matita_nat_minus.minus m (Matita_nat_nat.S(n))) n))))
  31 )
  32 ))) in div_aux
  33 ;;
  34
  35 let div =
  36 (function n -> (function m ->
  37 (match m with
  38    Matita_nat_nat.O -> (Matita_nat_nat.S(n))
  39  | Matita_nat_nat.S(p) -> (div_aux n n p))
  40 ))
  41 ;;
  42
  43 let div_mod_spec_rec =
  44 (function n -> (function n1 -> (function n2 -> (function n3 -> (function f -> (f))))))
  45 ;;
  46
  47 let div_mod_spec_rect =
  48 (function n -> (function n1 -> (function n2 -> (function n3 -> (function f -> (f))))))
  49 ;;
  50
  51 let n_divides_aux =
  52 let rec n_divides_aux =
  53 (function p -> (function n -> (function m -> (function acc ->
  54 (match (mod_ n m) with
  55    Matita_nat_nat.O ->
  56 (match p with
  57    Matita_nat_nat.O -> (Matita_datatypes_constructors.Pair(acc,n))
  58  | Matita_nat_nat.S(p) -> (n_divides_aux p (div n m) m (Matita_nat_nat.S(acc))))
  59
  60  | Matita_nat_nat.S(a) -> (Matita_datatypes_constructors.Pair(acc,n)))
  61 )))) in n_divides_aux
  62 ;;
  63
  64 let n_divides =
  65 (function n -> (function m -> (n_divides_aux n n m Matita_nat_nat.O)))
  66 ;;
  67