source: Deliverables/D3.1/C-semantics/Graphs.ma @ 639

Last change on this file since 639 was 639, checked in by campbell, 10 years ago

Preliminary work on RTLabs semantics
Will move to somewhere more appropriate 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.