lstar removed from list.ma and placed in its own file

[helm.git] / matita / matita / contribs / lambda / policy.txt

diff --git a/matita/matita/contribs/lambda/policy.txt b/matita/matita/contribs/lambda/policy.txt
index 77b0fdab7ad30c82bc0e63d25125e2a0a521391e..9f74e233918ad99ae79f068ed4d4796e0a10ab0d 100644 (file)
--- a/matita/matita/contribs/lambda/policy.txt
+++ b/matita/matita/contribs/lambda/policy.txt
@@ -4,12 +4,16 @@ A, B, C, D: term
 H         : transient premise
 IH        : inductive premise
 M, N      : term
+R         : arbitrary relation
+T, U      : arbitrary small type
 
 a, b      : boolean
 d, e      : variable reference depth 
 h         : relocation height
 i, j      : de Bruijn index
 k         : relocation height
+l         : arbitrary list
 m, n      : measures on terms
 p, q      : redex pointer
 r, s      : redex pointer sequence
+t, u      : arbitrary element