extracted/extranat.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 open Bool
  14
  15 open Relations
  16
  17 open Nat
  18
  19 open Jmeq
  20
  21 open Russell
  22
  23 open List
  24
  25 open Setoids
  26
  27 open Monad
  28
  29 open Option
  30
  31 val nat_bound_opt : Nat.nat -> Nat.nat -> __ Types.option
  32
  33 type nat_compared =
  34 | Nat_lt of Nat.nat * Nat.nat
  35 | Nat_eq of Nat.nat
  36 | Nat_gt of Nat.nat * Nat.nat
  37
  38 val nat_compared_rect_Type4 :
  39   (Nat.nat -> Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> Nat.nat ->
  40   'a1) -> Nat.nat -> Nat.nat -> nat_compared -> 'a1
  41
  42 val nat_compared_rect_Type5 :
  43   (Nat.nat -> Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> Nat.nat ->
  44   'a1) -> Nat.nat -> Nat.nat -> nat_compared -> 'a1
  45
  46 val nat_compared_rect_Type3 :
  47   (Nat.nat -> Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> Nat.nat ->
  48   'a1) -> Nat.nat -> Nat.nat -> nat_compared -> 'a1
  49
  50 val nat_compared_rect_Type2 :
  51   (Nat.nat -> Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> Nat.nat ->
  52   'a1) -> Nat.nat -> Nat.nat -> nat_compared -> 'a1
  53
  54 val nat_compared_rect_Type1 :
  55   (Nat.nat -> Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> Nat.nat ->
  56   'a1) -> Nat.nat -> Nat.nat -> nat_compared -> 'a1
  57
  58 val nat_compared_rect_Type0 :
  59   (Nat.nat -> Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> Nat.nat ->
  60   'a1) -> Nat.nat -> Nat.nat -> nat_compared -> 'a1
  61
  62 val nat_compared_inv_rect_Type4 :
  63   Nat.nat -> Nat.nat -> nat_compared -> (Nat.nat -> Nat.nat -> __ -> __ -> __
  64   -> 'a1) -> (Nat.nat -> __ -> __ -> __ -> 'a1) -> (Nat.nat -> Nat.nat -> __
  65   -> __ -> __ -> 'a1) -> 'a1
  66
  67 val nat_compared_inv_rect_Type3 :
  68   Nat.nat -> Nat.nat -> nat_compared -> (Nat.nat -> Nat.nat -> __ -> __ -> __
  69   -> 'a1) -> (Nat.nat -> __ -> __ -> __ -> 'a1) -> (Nat.nat -> Nat.nat -> __
  70   -> __ -> __ -> 'a1) -> 'a1
  71
  72 val nat_compared_inv_rect_Type2 :
  73   Nat.nat -> Nat.nat -> nat_compared -> (Nat.nat -> Nat.nat -> __ -> __ -> __
  74   -> 'a1) -> (Nat.nat -> __ -> __ -> __ -> 'a1) -> (Nat.nat -> Nat.nat -> __
  75   -> __ -> __ -> 'a1) -> 'a1
  76
  77 val nat_compared_inv_rect_Type1 :
  78   Nat.nat -> Nat.nat -> nat_compared -> (Nat.nat -> Nat.nat -> __ -> __ -> __
  79   -> 'a1) -> (Nat.nat -> __ -> __ -> __ -> 'a1) -> (Nat.nat -> Nat.nat -> __
  80   -> __ -> __ -> 'a1) -> 'a1
  81
  82 val nat_compared_inv_rect_Type0 :
  83   Nat.nat -> Nat.nat -> nat_compared -> (Nat.nat -> Nat.nat -> __ -> __ -> __
  84   -> 'a1) -> (Nat.nat -> __ -> __ -> __ -> 'a1) -> (Nat.nat -> Nat.nat -> __
  85   -> __ -> __ -> 'a1) -> 'a1
  86
  87 val nat_compared_discr :
  88   Nat.nat -> Nat.nat -> nat_compared -> nat_compared -> __
  89
  90 val nat_compared_jmdiscr :
  91   Nat.nat -> Nat.nat -> nat_compared -> nat_compared -> __
  92
  93 val nat_compare : Nat.nat -> Nat.nat -> nat_compared
  94
  95 val eq_nat_dec : Nat.nat -> Nat.nat -> (__, __) Types.sum
  96