From ded933cd70fc158d915d6aff3bfc6f775fe09333 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 5 Sep 2005 12:04:50 +0000 Subject: [PATCH] Typing errors fixed. --- helm/matita/contribs/LAMBDA-TYPES/tlt_defs.ma | 20 +++++++++---------- 1 file changed, 9 insertions(+), 11 deletions(-) diff --git a/helm/matita/contribs/LAMBDA-TYPES/tlt_defs.ma b/helm/matita/contribs/LAMBDA-TYPES/tlt_defs.ma index f2bf3660d..09ae56ef8 100644 --- a/helm/matita/contribs/LAMBDA-TYPES/tlt_defs.ma +++ b/helm/matita/contribs/LAMBDA-TYPES/tlt_defs.ma @@ -23,11 +23,11 @@ definition wadd: (nat \to nat) \to nat \to (nat \to nat) \def | (S m) \Rightarrow (map m) ]. -let rec weight_map (A:Set) (N:Set) (map:nat \to nat) (t:T) : nat \def +let rec weight_map (A:Set) (N:Set) (map:nat \to nat) (t:T A N) on t : nat \def match t with [ - (TSort A N y k) \Rightarrow O - | (TLRef A N y i) \Rightarrow (map i) - | (TWag A N y z w u) \Rightarrow + (TSort y k) \Rightarrow O + | (TLRef y i) \Rightarrow (map i) + | (TWag y z w u) \Rightarrow match z with [ (Bind b) \Rightarrow match b with [ @@ -40,12 +40,10 @@ let rec weight_map (A:Set) (N:Set) (map:nat \to nat) (t:T) : nat \def ] | (Flat a) \Rightarrow (S (plus (weight_map A N map w) (weight_map A N map u))) - ]].(* - | (TGRef A N y n) \Rightarrow O - ].*) -(* - Definition weight : T \to nat := (weight_map [_](0)). + ] + | (TGRef y n) \Rightarrow O + ]. - Definition tlt : T \to T \to Prop := [t1,t2](lt (weight t1) (weight t2)). +definition weight : \forall A,N. T A N \to nat \def \lambda A,N.(weight_map A N (\lambda _.O)). -*) +definition tlt : \forall A,N. T A N \to T A N \to Prop \def \lambda A,N. \lambda t1,t2. (lt (weight A N t1) (weight A N t2)). \ No newline at end of file -- 2.39.2