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 R         : arbitrary relation
   8 T, U      : arbitrary small type
   9
  10 a, b      : boolean
  11 d, e      : variable reference depth
  12 h         : relocation height
  13 i, j      : de Bruijn index
  14 k         : relocation height
  15 l         : arbitrary list
  16 m, n      : measures on terms
  17 p, q      : redex pointer
  18 r, s      : redex pointer sequence
  19 t, u      : arbitrary element