source: src/common/Graphs.ma @ 1080

Last change on this file since 1080 was 1080, checked in by mulligan, 9 years ago

more added

File size: 685 bytes
Line 
1include "basics/types.ma".
2
3include "ASM/BitVectorTrie.ma".
4include "common/Identifiers.ma".
5
6axiom LabelTag : String.
7
8definition label ≝ identifier LabelTag.
9
10definition label_eq : ∀x,y:label. (x=y) + (x≠y) ≝ identifier_eq ?.
11
12definition graph : Type[0] → Type[0] ≝ identifier_map LabelTag.
13
14axiom graph_add:
15  ∀A: Type[0].
16  ∀g: graph A.
17  ∀l: label.
18  ∀s: A.
19    lookup ? ? (add ? ? g l s) l ≠ None ?.
20
21axiom graph_add_lookup:
22  ∀A: Type[0].
23  ∀g: graph A.
24  ∀l: label.
25  ∀s: A.
26  ∀to_insert: label.
27    lookup ? ? g l ≠ None ? → lookup ? ? (add ? ? g to_insert s) l ≠ None ?.
28
29axiom graph_num_nodes:
30  ∀A: Type[0].
31  ∀g: graph A.
32    nat.
Note: See TracBrowser for help on using the repository browser.