1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "Basic_2/grammar/aarity.ma".
16 include "Basic_2/substitution/ldrop.ma".
18 (* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************)
20 inductive aaa: lenv → term → predicate aarity ≝
21 | aaa_sort: ∀L,k. aaa L (⋆k) 𝕒
22 | aaa_lref: ∀I,L,K,V,B,i. ↓[0, i] L ≡ K. 𝕓{I} V → aaa K V B → aaa L (#i) B
23 | aaa_abbr: ∀L,V,T,B,A.
24 aaa L V B → aaa (L. 𝕓{Abbr} V) T A → aaa L (𝕔{Abbr} V. T) A
25 | aaa_abst: ∀L,V,T,B,A.
26 aaa L V B → aaa (L. 𝕓{Abst} V) T A → aaa L (𝕔{Abbr} V. T) (𝕔 B. A)
27 | aaa_appl: ∀L,V,T,B,A. aaa L V B → aaa L T (𝕔 B. A) → aaa L (𝕔{Appl} V. T) A
28 | aaa_cast: ∀L,V,T,A. aaa L V A → aaa L T A → aaa L (𝕔{Cast} V. T) A
32 "atomic arity assignment (term)"
33 'AtomicArity L T A = (aaa L T A).