Changeset 10 for Csemantics/Maps.ma
 Timestamp:
 Jul 6, 2010, 11:53:23 AM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Csemantics/Maps.ma
r3 r10 172 172 *) 173 173 174 naxiom PTree : TREE ident. 174 (* XXX: need real tree impl *) 175 nlet rec assoc_get (A:Type) (i:ident) (l:list (ident × A)) on l ≝ 176 match l with 177 [ nil ⇒ None ? 178  cons h t ⇒ 179 match h with [ mk_pair hi ha ⇒ 180 match ident_eq i hi with [ inl _ ⇒ Some ? ha  inr _ ⇒ assoc_get A i t ] ] 181 ]. 182 183 naxiom assoc_tree_eq: ∀A: Type. ∀x,y: A. (x=y) + (x≠y) → 184 ∀a,b: list (ident × A). (a = b) + (a ≠ b). 185 naxiom assoc_remove: ∀A: Type. ident → list (ident × A) → list (ident × A). 186 naxiom assoc_tree_map: ∀A,B: Type. (ident → A → B) → list (ident × A) → list (ident × B). 187 naxiom assoc_elements: ∀A: Type. list (ident × A) → list (ident × A). 188 naxiom assoc_tree_fold: ∀A,B: Type. (B → ident → A → B) → list (ident × A) → B → B. 189 190 ndefinition PTree : TREE ident ≝ 191 mk_TREE ? 192 ident_eq 193 (λA. list (ident × A)) 194 assoc_tree_eq 195 (λA. nil ?) 196 assoc_get 197 (λA,i,a,l.〈i,a〉::l) 198 assoc_remove 199 assoc_tree_map 200 assoc_elements 201 assoc_tree_fold. 175 202 176 203 (*
Note: See TracChangeset
for help on using the changeset viewer.