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

   1 let sigma =
   2 let rec sigma =
   3 (function n -> (function f -> (function m ->
   4 (match n with
   5    Matita_nat_nat.O -> (f m)
   6  | Matita_nat_nat.S(p) -> (Matita_nat_plus.plus (f (Matita_nat_plus.plus (Matita_nat_nat.S(p)) m)) (sigma p f m)))
   7 ))) in sigma
   8 ;;
   9
  10 let pi =
  11 let rec pi =
  12 (function n -> (function f -> (function m ->
  13 (match n with
  14    Matita_nat_nat.O -> (f m)
  15  | Matita_nat_nat.S(p) -> (Matita_nat_times.times (f (Matita_nat_plus.plus (Matita_nat_nat.S(p)) m)) (pi p f m)))
  16 ))) in pi
  17 ;;
  18