From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 18 Apr 2008 18:31:58 +0000 (+0000)
Subject: Dead code removed.
X-Git-Tag: make_still_working~5318
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a7d6e83ed805988b82f35e8f39934855b156f97a;p=helm.git

Dead code removed.
---

diff --git a/helm/software/matita/contribs/POPLmark/Fsub/defn.ma b/helm/software/matita/contribs/POPLmark/Fsub/defn.ma
index 3bd8d2bdc..7907405ff 100644
--- a/helm/software/matita/contribs/POPLmark/Fsub/defn.ma
+++ b/helm/software/matita/contribs/POPLmark/Fsub/defn.ma
@@ -44,16 +44,6 @@ let rec subst_type_nat T U i \def
     | (Arrow T1 T2) \Rightarrow (Arrow (subst_type_nat T1 U i) (subst_type_nat T2 U i))
     | (Forall T1 T2) \Rightarrow (Forall (subst_type_nat T1 U i) (subst_type_nat T2 U (S i))) ].
 
-(*** height of T's syntactic tree ***)
-
-let rec t_len T \def
-  match T with
-     [(TVar n) \Rightarrow (S O)
-     |(TFree X) \Rightarrow (S O)
-     |Top \Rightarrow (S O)
-     |(Arrow T1 T2) \Rightarrow (S (max (t_len T1) (t_len T2)))
-     |(Forall T1 T2) \Rightarrow (S (max (t_len T1) (t_len T2)))].
-
 (*** definitions about lists ***)
 
 definition fv_env : (list bound) \to (list nat) \def
@@ -147,11 +137,6 @@ notation "hvbox(S [# n ↦ T])"
 interpretation "subst bound var" 'substvar S T n =
   (cic:/matita/Fsub/defn/subst_type_nat.con S T n).  
 
-notation "hvbox(|T|)"
-  non associative with precedence 30 for @{ 'tlen $T }.
-interpretation "type length" 'tlen T =
-  (cic:/matita/Fsub/defn/t_len.con T).  
-
 notation "hvbox(!X ⊴ T)"
   non associative with precedence 60 for @{ 'subtypebound $X $T }.
 interpretation "subtyping bound" 'subtypebound X T =
@@ -390,4 +375,4 @@ qed.
 
 lemma fv_append : ∀G,H.fv_env (G @ H) = (fv_env G @ fv_env H).
 intro;elim G;simplify;autobatch paramodulation;
-qed.
\ No newline at end of file
+qed.