Changeset 2541
- Timestamp:
- Dec 6, 2012, 4:02:36 PM (7 years ago)
- Location:
- src/common
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
src/common/Identifiers.ma
r2439 r2541 740 740 λtag,A,s.match s with [an_id_map p ⇒ |p|]. 741 741 742 interpretation "identifier map domain size" ' norms = (id_map_size ?? s).742 interpretation "identifier map domain size" 'card s = (id_map_size ?? s). 743 743 744 744 lemma set_eq_ext_empty_to_card : ∀tag,A.∀s : identifier_map tag A. (∀i.i∈s = false) → |s| = 0. -
src/common/PositiveMap.ma
r2453 r2541 487 487 ]. 488 488 489 (* just to load notation for 'norm (list.ma's notation overrides core's 'card)*) 490 include "basics/lists/list.ma". 491 interpretation "positive map size" 'norm p = (domain_size ? p). 489 interpretation "positive map size" 'card p = (domain_size ? p). 492 490 493 491 lemma map_opt_size : ∀A,B,f,b.|map_opt A B f b| ≤ |b|.
Note: See TracChangeset
for help on using the changeset viewer.