From f04a064bb34aabaf91dc0c48e3b08b37ecd7b0a2 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Thu, 10 Feb 2011 15:41:24 +0000
Subject: [PATCH] we added some comments

---
 matita/matita/lib/lambda/subst.ma | 16 ++++++----------
 matita/matita/lib/lambda/types.ma |  8 --------
 2 files changed, 6 insertions(+), 18 deletions(-)

diff --git a/matita/matita/lib/lambda/subst.ma b/matita/matita/lib/lambda/subst.ma
index 85bef55e1..bd8c5b713 100644
--- a/matita/matita/lib/lambda/subst.ma
+++ b/matita/matita/lib/lambda/subst.ma
@@ -12,14 +12,15 @@
 include "arithmetics/nat.ma".
 
 inductive T : Type[0] ≝
-  | Sort: nat → T
-  | Rel: nat → T 
-  | App: T → T → T 
+  | Sort: nat → T     (* starts from 0 *)
+  | Rel: nat → T      (* starts from ... ? *)
+  | App: T → T → T    (* function, argument *)
   | Lambda: T → T → T (* type, body *)
-  | Prod: T → T → T (* type, body *)
-  | D: T →T
+  | Prod: T → T → T   (* type, body *)
+  | D: T → T          (* dummifier *)
 .
 
+(* arguments: k is the depth (starts from 0), p is the height (starts from 0) *)
 let rec lift t k p ≝
   match t with 
     [ Sort n ⇒ Sort n
@@ -227,8 +228,3 @@ lemma subst_lemma: ∀A,B,C.∀k,i.
     ]
   ] 
 qed.
-
-  
-
-
-
diff --git a/matita/matita/lib/lambda/types.ma b/matita/matita/lib/lambda/types.ma
index 2a89549d6..543b3b7b9 100644
--- a/matita/matita/lib/lambda/types.ma
+++ b/matita/matita/lib/lambda/types.ma
@@ -212,11 +212,3 @@ theorem substitution_tj:
    #G1 #D #N #Heq #tjN @dummy /2/ 
   ]
 qed.
- 
-  
- 
-
-
-
-
-
-- 
2.39.2