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

Rev  Line  

[639]  1  

 2  include "basics/logic.ma". 

 3  

 4  include "binary/positive.ma". 

 5  include "Maps.ma". 

 6  

 7  definition label : Type[0] ≝ Pos. 

 8  definition graph : Type[0] → Type[0] ≝ tree_t … PTree. 

 9  definition graph_lookup : ∀T. graph T → label → option T ≝ 

 10  λT,g,l. get … l g. 

 11  

 12  

 13  definition 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  

 17  record label_generation : Type[0] ≝ { label_next : label }. 

 18  

 19  definition 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.