extracted/extralib.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 List
  20
  21 open Div_and_mod
  22
  23 open Jmeq
  24
  25 open Russell
  26
  27 open Util
  28
  29 val eq_rect_Type0_r : 'a1 -> 'a2 -> 'a1 -> 'a2
  30
  31 val eq_rect_r2 : 'a1 -> 'a1 -> 'a2 -> 'a2
  32
  33 val eq_rect_Type2_r : 'a1 -> 'a2 -> 'a1 -> 'a2
  34
  35 val dec_bounded_forall :
  36   (Nat.nat -> (__, __) Types.sum) -> Nat.nat -> (__, __) Types.sum
  37
  38 val dec_bounded_exists :
  39   (Nat.nat -> (__, __) Types.sum) -> Nat.nat -> (__, __) Types.sum
  40
  41 val dec_true : (__, __) Types.sum -> (__ -> 'a1) -> 'a1
  42
  43 val dec_false : (__, __) Types.sum -> (__ -> 'a1) -> 'a1
  44