- notation change for weight functions (following lambda)

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / static / aaa.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/static/aaa.ma
index b5f416344d5545ec866769b316e77ac0a9fae805..f9a98fec1774767218ef95d981c0100fe619c9c9 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/static/aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/aaa.ma
@@ -18,7 +18,7 @@ include "basic_2/substitution/ldrop.ma".
 (* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************)
 
 inductive aaa: lenv → term → predicate aarity ≝
-| aaa_sort: ∀L,k. aaa L (⋆k) ⓪
+| aaa_sort: ∀L,k. aaa L (⋆k) (⓪)
 | aaa_lref: ∀I,L,K,V,B,i. ⇩[0, i] L ≡ K. ⓑ{I} V → aaa K V B → aaa L (#i) B
 | aaa_abbr: ∀a,L,V,T,B,A.
             aaa L V B → aaa (L. ⓓV) T A → aaa L (ⓓ{a}V. T) A