matita/matita/contribs/lambda/policy.txt

   1 NAMING CONVENTIONS FOR METAVARIABLES
   2
   3 A, B, C, D: term
   4 H         : transient premise
   5 IH        : inductive premise
   6 M, N      : term
   7
   8 a, b      : boolean
   9 d, e      : variable reference depth
  10 h         : relocation height
  11 i, j      : de Bruijn index
  12 k         : relocation height
  13 m, n      : measures on terms
  14 p, q      : redex pointer
  15 r, s      : redex pointer sequence