X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fnames.txt;h=c24186766a4a8658bdbd65170665401a3a03300c;hb=3c8da07d7a5d7cf0432a83732a6d103f527afaef;hp=fbf3612a6a7e8a7eaa03b618b5c878efa4b5c686;hpb=7632da8aa4f6751e351546be3d90fb23f634108c;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/basic_2/names.txt b/matita/matita/contribs/lambdadelta/basic_2/names.txt index fbf3612a6..c24186766 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/names.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/names.txt @@ -24,8 +24,7 @@ f,g : local reference transforming map h : sort hierarchy parameter i,j : local reference depth (de Bruijn's) k,l : global reference level -m : -n : type iterations +m,n : iterations o : sort degree parameter (origin) p,q : binder polarity r : @@ -40,6 +39,7 @@ NAMING CONVENTIONS FOR CONSTRUCTORS 2: binary A: application to vector +E: empty list F: boolean false T: boolean true @@ -47,6 +47,7 @@ a: application b: generic binder with one argument d: abbreviation f: generic flat with one argument +i: generic binder for local environments l: typed abstraction n: native type annotation u: generic binder with zero argument