Changeset 1555 for src/common


Ignore:
Timestamp:
Nov 24, 2011, 5:19:30 PM (8 years ago)
Author:
boender
Message:
  • changes to assembly
  • added lookup to PositiveMap?
  • lightly changed Fetch to make it compile
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/PositiveMap.ma

    r1516 r1555  
    1818].
    1919
     20definition lookup: ∀A:Type[0].Pos → positive_map A → A → A ≝ 
     21 λA.λb.λt.λx.
     22 match lookup_opt A b t with
     23 [ None ⇒ x
     24 | Some r ⇒ r
     25 ].
     26 
    2027let rec insert (A:Type[0]) (b:Pos) (a:A) (t:positive_map A) on b : positive_map A ≝
    2128match b with
Note: See TracChangeset for help on using the changeset viewer.