From f04a064bb34aabaf91dc0c48e3b08b37ecd7b0a2 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi 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