Changeset 1555 for src/common
- Timestamp:
- Nov 24, 2011, 5:19:30 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/common/PositiveMap.ma
r1516 r1555 18 18 ]. 19 19 20 definition 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 20 27 let rec insert (A:Type[0]) (b:Pos) (a:A) (t:positive_map A) on b : positive_map A ≝ 21 28 match b with
Note: See TracChangeset
for help on using the changeset viewer.