- notation (possibly affecting all .ma files):

[helm.git] / matita / matita / re_complete / basics / list.ma

diff --git a/matita/matita/re_complete/basics/list.ma b/matita/matita/re_complete/basics/list.ma
index b0a6831356957f897782355324122a2fea5c12a5..df0fa840cb6b3d7252ead27b5bc781d7aceccb62 100644 (file)
--- a/matita/matita/re_complete/basics/list.ma
+++ b/matita/matita/re_complete/basics/list.ma
@@ -151,7 +151,7 @@ let rec length (A:Type[0]) (l:list A) on l ≝
     [ nil ⇒ O
     | cons a tl ⇒ S (length A tl)].
 
-notation "|M|" non associative with precedence 60 for @{'norm $M}.
+notation "|M|" non associative with precedence 65 for @{'norm $M}.
 interpretation "norm" 'norm l = (length ? l).
 
 lemma length_append: ∀A.∀l1,l2:list A.