source: driver/extracted/deqsets_extra.ml @ 3106

Last change on this file since 3106 was 2730, checked in by sacerdot, 7 years ago

Exported again.

File size: 454 bytes
Line 
1open Preamble
2
3open Relations
4
5open Bool
6
7open Hints_declaration
8
9open Core_notation
10
11open Pts
12
13open Logic
14
15open Types
16
17open Deqsets
18
19open Sets
20
21open Nat
22
23open List
24
25open Listb
26
27open Div_and_mod
28
29open Jmeq
30
31open Russell
32
33open Util
34
35(** val eqb_elim :
36    Deqsets.deqSet -> __ -> __ -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
37let 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
Note: See TracBrowser for help on using the repository browser.