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

   1 type void = unit (* empty type *)
   2 ;;
   3
   4 let void_rec =
   5 (function v -> assert false)
   6 ;;
   7
   8 let void_rect =
   9 (function v -> assert false)
  10 ;;
  11
  12 type unit =
  13 Something
  14 ;;
  15
  16 let unit_rec =
  17 (function p -> (function u ->
  18 (match u with
  19    Something -> p)
  20 ))
  21 ;;
  22
  23 let unit_rect =
  24 (function p -> (function u ->
  25 (match u with
  26    Something -> p)
  27 ))
  28 ;;
  29
  30 type ('a,'b) prod =
  31 Pair of 'a * 'b
  32 ;;
  33
  34 let prod_rec =
  35 (function f -> (function p ->
  36 (match p with
  37    Pair(t,t1) -> (f t t1))
  38 ))
  39 ;;
  40
  41 let prod_rect =
  42 (function f -> (function p ->
  43 (match p with
  44    Pair(t,t1) -> (f t t1))
  45 ))
  46 ;;
  47
  48 let fst =
  49 (function p ->
  50 (match p with
  51    Pair(a,b) -> a)
  52 )
  53 ;;
  54
  55 let snd =
  56 (function p ->
  57 (match p with
  58    Pair(a,b) -> b)
  59 )
  60 ;;
  61
  62 type ('a,'b) sum =
  63 Inl of 'a
  64  | Inr of 'b
  65 ;;
  66
  67 let sum_rec =
  68 (function f -> (function f1 -> (function s ->
  69 (match s with
  70    Inl(t) -> (f t)
  71  | Inr(t) -> (f1 t))
  72 )))
  73 ;;
  74
  75 let sum_rect =
  76 (function f -> (function f1 -> (function s ->
  77 (match s with
  78    Inl(t) -> (f t)
  79  | Inr(t) -> (f1 t))
  80 )))
  81 ;;
  82
  83 type ('a) option =
  84 None
  85  | Some of 'a
  86 ;;
  87
  88 let option_rec =
  89 (function p -> (function f -> (function o ->
  90 (match o with
  91    None -> p
  92  | Some(t) -> (f t))
  93 )))
  94 ;;
  95
  96 let option_rect =
  97 (function p -> (function f -> (function o ->
  98 (match o with
  99    None -> p
 100  | Some(t) -> (f t))
 101 )))
 102 ;;
 103