X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Flambda%2Fpolicy.txt;fp=matita%2Fmatita%2Flib%2Flambda%2Fpolicy.txt;h=9e64369a9b01b2405ee9bc1df712c25cf54d582b;hb=aa9654656f7d0aeb9345e0b86a9e35f861687580;hp=0000000000000000000000000000000000000000;hpb=637ff9311e16f1d58e03d873f84c354e1cf1e716;p=helm.git

diff --git a/matita/matita/lib/lambda/policy.txt b/matita/matita/lib/lambda/policy.txt
new file mode 100644
index 000000000..9e64369a9
--- /dev/null
+++ b/matita/matita/lib/lambda/policy.txt
@@ -0,0 +1,24 @@
+NAMING CONVENTIONS FOR METAVARIABLES
+
+A, B, C, D: term
+F,G       : subset of subterms
+H         : transient premise
+IH        : inductive premise
+M, N      : term
+P, Q      : pointer tree
+R         : arbitrary relation
+S         : arbitrary small type
+T, U, V, W: subset of subterms
+
+a         : arbitrary element
+b,c       : boolean mark
+d, e      : variable reference level
+f         : arbitrary function
+h         : relocation height
+i, j      : variable reference depth (de Bruijn index)
+k         : relocation height
+l         : arbitrary list
+m, n      : measures on terms
+o         : pointer step
+p, q      : pointer
+r, s      : pointer sequence