extracted/order.mli

   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
  20 val order_rect_Type5 : 'a1 -> 'a1 -> 'a1 -> order -> 'a1
  21
  22 val order_rect_Type3 : 'a1 -> 'a1 -> 'a1 -> order -> 'a1
  23
  24 val order_rect_Type2 : 'a1 -> 'a1 -> 'a1 -> order -> 'a1
  25
  26 val order_rect_Type1 : 'a1 -> 'a1 -> 'a1 -> order -> 'a1
  27
  28 val order_rect_Type0 : 'a1 -> 'a1 -> 'a1 -> order -> 'a1
  29
  30 val order_inv_rect_Type4 :
  31   order -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
  32
  33 val order_inv_rect_Type3 :
  34   order -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
  35
  36 val order_inv_rect_Type2 :
  37   order -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
  38
  39 val order_inv_rect_Type1 :
  40   order -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
  41
  42 val order_inv_rect_Type0 :
  43   order -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
  44
  45 val order_discr : order -> order -> __
  46