extracted/extra_bool.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 Relations
  12
  13 open Bool
  14
  15 open Div_and_mod
  16
  17 open Jmeq
  18
  19 open Russell
  20
  21 open Nat
  22
  23 open Types
  24
  25 open List
  26
  27 open Util
  28
  29 (** val if_elim :
  30     Bool.bool -> 'a1 -> 'a1 -> (__ -> 'a2) -> (__ -> 'a2) -> 'a2 **)
  31 let if_elim clearme e1 e2 x x0 =
  32   (match clearme with
  33    | Bool.True -> (fun e3 e4 _ auto auto' -> auto __)
  34    | Bool.False -> (fun e3 e4 _ auto auto' -> auto' __)) e1 e2 __ x x0
  35