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