extracted/order.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 Types
  12
  13 type order =
  14 | Order_lt
  15 | Order_eq
  16 | Order_gt
  17
  18 (** val order_rect_Type4 : 'a1 -> 'a1 -> 'a1 -> order -> 'a1 **)
  19 let rec order_rect_Type4 h_order_lt h_order_eq h_order_gt = function
  20 | Order_lt -> h_order_lt
  21 | Order_eq -> h_order_eq
  22 | Order_gt -> h_order_gt
  23
  24 (** val order_rect_Type5 : 'a1 -> 'a1 -> 'a1 -> order -> 'a1 **)
  25 let rec order_rect_Type5 h_order_lt h_order_eq h_order_gt = function
  26 | Order_lt -> h_order_lt
  27 | Order_eq -> h_order_eq
  28 | Order_gt -> h_order_gt
  29
  30 (** val order_rect_Type3 : 'a1 -> 'a1 -> 'a1 -> order -> 'a1 **)
  31 let rec order_rect_Type3 h_order_lt h_order_eq h_order_gt = function
  32 | Order_lt -> h_order_lt
  33 | Order_eq -> h_order_eq
  34 | Order_gt -> h_order_gt
  35
  36 (** val order_rect_Type2 : 'a1 -> 'a1 -> 'a1 -> order -> 'a1 **)
  37 let rec order_rect_Type2 h_order_lt h_order_eq h_order_gt = function
  38 | Order_lt -> h_order_lt
  39 | Order_eq -> h_order_eq
  40 | Order_gt -> h_order_gt
  41
  42 (** val order_rect_Type1 : 'a1 -> 'a1 -> 'a1 -> order -> 'a1 **)
  43 let rec order_rect_Type1 h_order_lt h_order_eq h_order_gt = function
  44 | Order_lt -> h_order_lt
  45 | Order_eq -> h_order_eq
  46 | Order_gt -> h_order_gt
  47
  48 (** val order_rect_Type0 : 'a1 -> 'a1 -> 'a1 -> order -> 'a1 **)
  49 let rec order_rect_Type0 h_order_lt h_order_eq h_order_gt = function
  50 | Order_lt -> h_order_lt
  51 | Order_eq -> h_order_eq
  52 | Order_gt -> h_order_gt
  53
  54 (** val order_inv_rect_Type4 :
  55     order -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
  56 let order_inv_rect_Type4 hterm h1 h2 h3 =
  57   let hcut = order_rect_Type4 h1 h2 h3 hterm in hcut __
  58
  59 (** val order_inv_rect_Type3 :
  60     order -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
  61 let order_inv_rect_Type3 hterm h1 h2 h3 =
  62   let hcut = order_rect_Type3 h1 h2 h3 hterm in hcut __
  63
  64 (** val order_inv_rect_Type2 :
  65     order -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
  66 let order_inv_rect_Type2 hterm h1 h2 h3 =
  67   let hcut = order_rect_Type2 h1 h2 h3 hterm in hcut __
  68
  69 (** val order_inv_rect_Type1 :
  70     order -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
  71 let order_inv_rect_Type1 hterm h1 h2 h3 =
  72   let hcut = order_rect_Type1 h1 h2 h3 hterm in hcut __
  73
  74 (** val order_inv_rect_Type0 :
  75     order -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
  76 let order_inv_rect_Type0 hterm h1 h2 h3 =
  77   let hcut = order_rect_Type0 h1 h2 h3 hterm in hcut __
  78
  79 (** val order_discr : order -> order -> __ **)
  80 let order_discr x y =
  81   Logic.eq_rect_Type2 x
  82     (match x with
  83      | Order_lt -> Obj.magic (fun _ dH -> dH)
  84      | Order_eq -> Obj.magic (fun _ dH -> dH)
  85      | Order_gt -> Obj.magic (fun _ dH -> dH)) y
  86