Changeset 2541

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:

• Identifiers.ma (modified) (1 diff)
• PositiveMap.ma (modified) (1 diff)

src/common/Identifiers.ma

@@ -740 +740 @@
   λtag,A,s.match s with [an_id_map p ⇒ |p|].
 
-interpretation "identifier map domain size" 'norm s = (id_map_size ?? s).
+interpretation "identifier map domain size" 'card s = (id_map_size ?? s).
 
 lemma set_eq_ext_empty_to_card : ∀tag,A.∀s : identifier_map tag A. (∀i.i∈s = false) → |s| = 0.

src/common/PositiveMap.ma

@@ -487 +487 @@
 ].
 
-(* just to load notation for 'norm (list.ma's notation overrides core's 'card)*)
-include "basics/lists/list.ma".
-interpretation "positive map size" 'norm p = (domain_size ? p).
+interpretation "positive map size" 'card p = (domain_size ? p).
 
 lemma map_opt_size : ∀A,B,f,b.|map_opt A B f b| ≤ |b|.