Changeset 2541 for src/common


Ignore:
Timestamp:
Dec 6, 2012, 4:02:36 PM (7 years ago)
Author:
tranquil
Message:

adapted size notation to last matita lib update (01/12/2012)
that removed 'norm interpretation
Beware: will not work without updating matita's lib

Location:
src/common
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/common/Identifiers.ma

    r2439 r2541  
    740740  λtag,A,s.match s with [an_id_map p ⇒ |p|].
    741741
    742 interpretation "identifier map domain size" 'norm s = (id_map_size ?? s).
     742interpretation "identifier map domain size" 'card s = (id_map_size ?? s).
    743743
    744744lemma 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  
    487487].
    488488
    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).
     489interpretation "positive map size" 'card p = (domain_size ? p).
    492490
    493491lemma map_opt_size : ∀A,B,f,b.|map_opt A B f b| ≤ |b|.
Note: See TracChangeset for help on using the changeset viewer.