Changeset 1555 for src/common

Timestamp:

Nov 24, 2011, 5:19:30 PM (9 years ago)

Author:

boender

Message:

• changes to assembly
• added lookup to PositiveMap?
• lightly changed Fetch to make it compile

File:

• src/common/PositiveMap.ma (modified) (1 diff)

src/common/PositiveMap.ma

@@ -18 +18 @@
 ].
 
+definition lookup: ∀A:Type[0].Pos → positive_map A → A → A ≝  
+ λA.λb.λt.λx.
+ match lookup_opt A b t with
+ [ None ⇒ x
+ | Some r ⇒ r
+ ].
+ 
 let rec insert (A:Type[0]) (b:Pos) (a:A) (t:positive_map A) on b : positive_map A ≝
 match b with