]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambda/multiplicity.ma
bug fix in notation precedences
[helm.git] / matita / matita / contribs / lambda / multiplicity.ma
index d6d5af1101f9f02493b094fa1cc9f4cc8ca6fd98..e8b72762b947e78b268b69cac1809de62e6be328 100644 (file)
@@ -26,8 +26,8 @@ let rec mult M on M ≝ match M with
 interpretation "multiplicity"
    'Multiplicity M = (mult M).
 
-notation "hvbox( #{M} )"
-   non associative with precedence 55
+notation "hvbox( #{ term 46 M } )"
+   non associative with precedence 90
    for @{ 'Multiplicity $M }.
 
 lemma mult_positive: ∀M. 0 < #{M}.