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/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.