Changeset 2104 for src/common/PositiveMap.ma
- Timestamp:
- Jun 21, 2012, 5:21:03 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/common/PositiveMap.ma
r1882 r2104 77 77 ] qed. 78 78 79 axiomlookup_insert_hit:79 lemma lookup_insert_hit: 80 80 ∀a: Type[0]. 81 81 ∀v: a. … … 84 84 ∀d: a. 85 85 lookup … b (insert … b v t) d = v. 86 #A #v #b #t #d whd in ⊢ (??%?); >lookup_opt_insert_hit % 87 qed. 86 88 87 89 lemma lookup_opt_insert_miss:
Note: See TracChangeset
for help on using the changeset viewer.