Cleared unused variables in wsem_match (they were also sharing names with

[helm.git] / matita / matita / lib / basics / lists / list.ma

diff --git a/matita/matita/lib/basics/lists/list.ma b/matita/matita/lib/basics/lists/list.ma
index a330f6224ef1fdb6c94e356b71955f9bad0129e5..5d000e5c19a81a7e6869da8214d4d65a3d31fc67 100644 (file)
--- 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 //