source: src/utilities/adt/set_adt.ma @ 2772

Last change on this file since 2772 was 2772, checked in by sacerdot, 8 years ago

Useless code removed.

File size: 831 bytes
Line 
1include "basics/types.ma".
2include "basics/lists/list.ma".
3include "arithmetics/nat.ma".
4include "ASM/Util.ma".
5
6axiom set: Type[0] → Type[0].
7
8axiom set_empty: ∀elt_type. set elt_type.
9
10axiom set_equal: ∀elt_type: Type[0]. (elt_type → elt_type → bool) →
11  set elt_type → set elt_type → bool.
12
13axiom set_subset: ∀elt_type: Type[0]. (elt_type → elt_type → bool) →
14 set elt_type → set elt_type → bool.
15
16axiom set_singleton: ∀elt_type: Type[0]. elt_type → set elt_type.
17
18axiom set_union: ∀elt_type: Type[0]. elt_type → elt_type → elt_type.
19
20axiom set_diff: ∀elt_type: Type[0]. elt_type → elt_type → elt_type.
21
22axiom set_from_list: ∀elt_type: Type[0]. list elt_type → set elt_type.
23
24axiom set_member: ∀elt_type. (elt_type → elt_type → bool) → elt_type → set elt_type → bool.
Note: See TracBrowser for help on using the repository browser.