source: src/common/Graphs.ma @ 695

Last change on this file since 695 was 695, checked in by campbell, 9 years ago

Rearrange Clight files a bit - will try to make them work again soon...

File size: 635 bytes
Line 
1
2include "basics/logic.ma".
3
4include "binary/positive.ma".
5include "Maps.ma".
6
7definition label : Type[0] ≝ Pos.
8definition graph : Type[0] → Type[0] ≝ tree_t … PTree.
9definition graph_lookup : ∀T. graph T → label → option T ≝
10λT,g,l. get … l g.
11
12
13definition label_eq : ∀x,y:label. (x=y) + (x≠y).
14#x #y lapply (pos_compare_to_Prop x y); cases (pos_compare x y);
15[ #H %2 /2/; | #H %1 //; | #H %2 /2/ ] qed.
16
17record label_generation : Type[0] ≝ { label_next : label }.
18
19definition label_new : label_generation → label × label_generation ≝
20λg. 〈label_next g, mk_label_generation (succ (label_next g))〉.
Note: See TracBrowser for help on using the repository browser.