extracted/bool.ml

   1 open Preamble
   2
   3 open Hints_declaration
   4
   5 open Core_notation
   6
   7 open Pts
   8
   9 open Logic
  10
  11 open Relations
  12
  13 type bool =
  14 | True
  15 | False
  16
  17 (** val bool_rect_Type4 : 'a1 -> 'a1 -> bool -> 'a1 **)
  18 let rec bool_rect_Type4 h_true h_false = function
  19 | True -> h_true
  20 | False -> h_false
  21
  22 (** val bool_rect_Type5 : 'a1 -> 'a1 -> bool -> 'a1 **)
  23 let rec bool_rect_Type5 h_true h_false = function
  24 | True -> h_true
  25 | False -> h_false
  26
  27 (** val bool_rect_Type3 : 'a1 -> 'a1 -> bool -> 'a1 **)
  28 let rec bool_rect_Type3 h_true h_false = function
  29 | True -> h_true
  30 | False -> h_false
  31
  32 (** val bool_rect_Type2 : 'a1 -> 'a1 -> bool -> 'a1 **)
  33 let rec bool_rect_Type2 h_true h_false = function
  34 | True -> h_true
  35 | False -> h_false
  36
  37 (** val bool_rect_Type1 : 'a1 -> 'a1 -> bool -> 'a1 **)
  38 let rec bool_rect_Type1 h_true h_false = function
  39 | True -> h_true
  40 | False -> h_false
  41
  42 (** val bool_rect_Type0 : 'a1 -> 'a1 -> bool -> 'a1 **)
  43 let rec bool_rect_Type0 h_true h_false = function
  44 | True -> h_true
  45 | False -> h_false
  46
  47 (** val bool_inv_rect_Type4 : bool -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
  48 let bool_inv_rect_Type4 hterm h1 h2 =
  49   let hcut = bool_rect_Type4 h1 h2 hterm in hcut __
  50
  51 (** val bool_inv_rect_Type3 : bool -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
  52 let bool_inv_rect_Type3 hterm h1 h2 =
  53   let hcut = bool_rect_Type3 h1 h2 hterm in hcut __
  54
  55 (** val bool_inv_rect_Type2 : bool -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
  56 let bool_inv_rect_Type2 hterm h1 h2 =
  57   let hcut = bool_rect_Type2 h1 h2 hterm in hcut __
  58
  59 (** val bool_inv_rect_Type1 : bool -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
  60 let bool_inv_rect_Type1 hterm h1 h2 =
  61   let hcut = bool_rect_Type1 h1 h2 hterm in hcut __
  62
  63 (** val bool_inv_rect_Type0 : bool -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
  64 let bool_inv_rect_Type0 hterm h1 h2 =
  65   let hcut = bool_rect_Type0 h1 h2 hterm in hcut __
  66
  67 (** val bool_discr : bool -> bool -> __ **)
  68 let bool_discr x y =
  69   Logic.eq_rect_Type2 x
  70     (match x with
  71      | True -> Obj.magic (fun _ dH -> dH)
  72      | False -> Obj.magic (fun _ dH -> dH)) y
  73
  74 (** val notb : bool -> bool **)
  75 let notb = function
  76 | True -> False
  77 | False -> True
  78
  79 (** val andb : bool -> bool -> bool **)
  80 let andb b1 b2 =
  81   match b1 with
  82   | True -> b2
  83   | False -> False
  84
  85 (** val orb : bool -> bool -> bool **)
  86 let orb b1 b2 =
  87   match b1 with
  88   | True -> True
  89   | False -> b2
  90
  91 (** val xorb : bool -> bool -> bool **)
  92 let xorb b1 b2 =
  93   match b1 with
  94   | True ->
  95     (match b2 with
  96      | True -> False
  97      | False -> True)
  98   | False ->
  99     (match b2 with
 100      | True -> True
 101      | False -> False)
 102