1 NAMING CONVENTIONS FOR METAVARIABLES
4 C,D : candidate of reducibility
7 H : reserved: transient premise
8 IH : reserved: inductive premise
10 K,L : local environment
11 M,N : reserved: future use
13 R : generic predicate (relation)
16 X,Y,Z : reserved: transient objet denoted by a capital letter
19 c : reserved: future use (lambda_delta 3)
23 g : sort degree parameter
24 h : sort hierarchy parameter
25 i,j : local reference position index (de Bruijn's)
28 m,n : reserved: future use
30 p,q : global reference position
32 t,u : local reference position level (de Bruijn's)
34 x,y,z : reserved: transient objet denoted by a small letter
36 NAMING CONVENTIONS FOR CONSTRUCTORS
41 A: application to vector
48 n: native type annotation
50 NAMING CONVENTIONS FOR TRANSFORMATIONS AND RELATED FORMS
54 c: contex-sensitive for terms
55 f: context-freee for closures
56 l: sn contex-sensitive for local environments
57 r: dx contex-sensitive for local environments
58 t: context-free for terms
64 p: parallel transformation
66 s: sequential transformation
71 d: decomposed extended reduction
72 q: restricted reduction
77 - forth letter (if present)
79 p: non-reflexive transitive closure (plus)
80 q: reflexive closure (question)
81 s: reflexive transitive closure (star)