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/syntax/term_weight.ma".
16 include "basic_2/syntax/bind.ma".
18 (* WEIGHT OF A BINDER FOR LOCAL ENVIRONMENTS *******************************)
20 rec definition bw I ≝ match I with
25 interpretation "weight (binder for local environments)" 'Weight I = (bw I).
27 (* Basic properties *********************************************************)
29 lemma bw_pos: ∀I. 1 ≤ ♯{I}.