]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/lib/lambda/policy.txt
update in delayed_updating
[helm.git] / matita / matita / lib / lambda / policy.txt
1 NAMING CONVENTIONS FOR METAVARIABLES
2
3 A, B, C, D: term
4 F,G       : subset of subterms
5 H         : transient premise
6 IH        : inductive premise
7 M, N      : term
8 P, Q      : pointer tree
9 R         : arbitrary relation
10 S         : arbitrary small type
11 T, U, V, W: subset of subterms
12
13 a         : arbitrary element
14 b,c       : boolean mark
15 d, e      : variable reference level
16 f         : arbitrary function
17 h         : relocation height
18 i, j      : variable reference depth (de Bruijn index)
19 k         : relocation height
20 l         : arbitrary list
21 m, n      : measures on terms
22 o         : pointer step
23 p, q      : pointer
24 r, s      : pointer sequence