X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fbasics%2Flists%2Flist.ma;h=5d000e5c19a81a7e6869da8214d4d65a3d31fc67;hb=4063c155ff95d3364fcdefb162f24d76b12c71a4;hp=a330f6224ef1fdb6c94e356b71955f9bad0129e5;hpb=5d54a6d3a0f22bb8784387c491de7bb66e67b625;p=helm.git

diff --git a/matita/matita/lib/basics/lists/list.ma b/matita/matita/lib/basics/lists/list.ma
index a330f6224..5d000e5c1 100644
--- a/matita/matita/lib/basics/lists/list.ma
+++ b/matita/matita/lib/basics/lists/list.ma
@@ -175,8 +175,7 @@ let rec length (A:Type[0]) (l:list A) on l ≝
     [ nil ⇒ 0
     | cons a tl ⇒ S (length A tl)].
 
-notation "|M|" non associative with precedence 65 for @{'norm $M}.
-interpretation "norm" 'norm l = (length ? l).
+interpretation "list length" 'card l = (length ? l).
 
 lemma length_tail: ∀A,l. length ? (tail A l) = pred (length ? l).
 #A #l elim l //