Ignore:
Timestamp:
Nov 25, 2011, 1:20:41 PM (9 years ago)
Author:
mulligan
Message:

new version of assembly, fixed conflict in positivemap.ma, changed erroneous axiom in identifiers.ma

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/PositiveMap.ma

    r1555 r1562  
    2424 | Some r ⇒ r
    2525 ].
    26  
     26
    2727let rec insert (A:Type[0]) (b:Pos) (a:A) (t:positive_map A) on b : positive_map A ≝
    2828match b with
     
    7777  ]
    7878] qed.
     79
     80axiom lookup_insert_hit:
     81  ∀a: Type[0].
     82  ∀v: a.
     83  ∀b: Pos.
     84  ∀t: positive_map a.
     85  ∀d: a.
     86    lookup … b (insert … b v t) d = v.
    7987
    8088lemma lookup_opt_insert_miss:
Note: See TracChangeset for help on using the changeset viewer.