extracted/extralib.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 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 let eq_rect_Type0_r a p x0 =
  31   Logic.eq_rect_r a x0 p
  32
  33 (** val eq_rect_r2 : 'a1 -> 'a1 -> 'a2 -> 'a2 **)
  34 let eq_rect_r2 a x x0 =
  35   (fun _ h -> h) __ x0
  36
  37 (** val eq_rect_Type2_r : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
  38 let eq_rect_Type2_r a p x0 =
  39   eq_rect_r2 a x0 p
  40
  41 (** val dec_bounded_forall :
  42     (Nat.nat -> (__, __) Types.sum) -> Nat.nat -> (__, __) Types.sum **)
  43 let dec_bounded_forall hP_dec k =
  44   Nat.nat_rect_Type0 (Types.Inl __) (fun k0 hind ->
  45     match hind with
  46     | Types.Inl _ ->
  47       (match hP_dec k0 with
  48        | Types.Inl _ -> Types.Inl __
  49        | Types.Inr _ -> Types.Inr __)
  50     | Types.Inr _ -> Types.Inr __) k
  51
  52 (** val dec_bounded_exists :
  53     (Nat.nat -> (__, __) Types.sum) -> Nat.nat -> (__, __) Types.sum **)
  54 let dec_bounded_exists hP_dec k =
  55   Nat.nat_rect_Type0 (Types.Inr __) (fun k0 hind ->
  56     match hind with
  57     | Types.Inl _ -> Types.Inl __
  58     | Types.Inr _ ->
  59       (match hP_dec k0 with
  60        | Types.Inl _ -> Types.Inl __
  61        | Types.Inr _ -> Types.Inr __)) k
  62
  63 (** val dec_true : (__, __) Types.sum -> (__ -> 'a1) -> 'a1 **)
  64 let dec_true f h =
  65   match f with
  66   | Types.Inl x -> h x
  67   | Types.Inr _ -> assert false (* absurd case *)
  68
  69 (** val dec_false : (__, __) Types.sum -> (__ -> 'a1) -> 'a1 **)
  70 let dec_false f h =
  71   match f with
  72   | Types.Inl _ -> assert false (* absurd case *)
  73   | Types.Inr x -> h x
  74