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

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

Unused code removed.

File size: 982 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
8inductive set (elt_type: Type[0]): Type[0] ≝
9  | empty: set elt_type
10  | node : nat → set elt_type → elt_type → set elt_type → set elt_type.
11
12axiom set_empty: ∀elt_type. set elt_type.
13
14axiom set_equal: ∀elt_type: Type[0]. (elt_type → elt_type → bool) →
15  set elt_type → set elt_type → bool.
16
17axiom set_subset: ∀elt_type: Type[0]. (elt_type → elt_type → bool) →
18 set elt_type → set elt_type → bool.
19
20axiom set_singleton: ∀elt_type: Type[0]. elt_type → set elt_type.
21
22axiom set_union: ∀elt_type: Type[0]. elt_type → elt_type → elt_type.
23
24axiom set_diff: ∀elt_type: Type[0]. elt_type → elt_type → elt_type.
25
26axiom set_from_list: ∀elt_type: Type[0]. list elt_type → set elt_type.
27
28axiom 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.