matita/matita/contribs/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         : boolean mark
  15 c         : pointer step
  16 d, e      : variable reference level
  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 p, q      : pointer
  23 r, s      : pointer sequence
  24