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

File:
1 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.
Note: See TracChangeset for help on using the changeset viewer.