extracted/deqsets_extra.ml

   1 open Preamble
   2
   3 open Relations
   4
   5 open Bool
   6
   7 open Hints_declaration
   8
   9 open Core_notation
  10
  11 open Pts
  12
  13 open Logic
  14
  15 open Types
  16
  17 open Deqsets
  18
  19 open Sets
  20
  21 open Nat
  22
  23 open List
  24
  25 open Listb
  26
  27 open Div_and_mod
  28
  29 open Jmeq
  30
  31 open Russell
  32
  33 open Util
  34
  35 (** val eqb_elim :
  36     Deqsets.deqSet -> __ -> __ -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
  37 let eqb_elim d x y t f =
  38   (match Deqsets.eqb d x y with
  39    | Bool.True -> (fun _ -> t __)
  40    | Bool.False -> (fun _ -> f __)) __
  41