- weight: bugfix + weight-based eliminator axiomatized

[helm.git] / matita / matita / lib / lambda-delta / language / weight.ma

diff --git a/matita/matita/lib/lambda-delta/language/weight.ma b/matita/matita/lib/lambda-delta/language/weight.ma
index d6d233dea1d25964e409d5f39b6f2073fe33619c..f6be4dab7d45b2897afe7bfe73a68f1ea1f526fe 100644 (file)
--- a/matita/matita/lib/lambda-delta/language/weight.ma
+++ b/matita/matita/lib/lambda-delta/language/weight.ma
@@ -31,6 +31,10 @@ let rec lw L ≝ match L with
 interpretation "weight (local environment)" 'Weight L = (lw L).
 
 (* the weight of a closure *)
-definition cw ≝ λL,T. #L + #T.
+definition cw: lenv → term → ? ≝ λL,T. #L + #T.
 
 interpretation "weight (closure)" 'Weight L T = (cw L T).
+
+axiom cw_wf_ind: ∀P:lenv→term→Prop.
+                 (∀L2,T2. (∀L1,T1. #[L1,T1] < #[L2,T2] → P L1 T1) → P L2 T2) →
+                 ∀L,T. P L T.