1 NAMING CONVENTIONS FOR METAVARIABLES
4 C : candidate of reducibility
6 F,G : global environment
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
21 e : 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)
31 p,q : global reference position
32 r : reduction kind parameter (true = ordinary, false = extended)
33 s : local dropping kind parameter (true = general, false = restricted)
34 t,u : local reference position level (de Bruijn's) (RTM)
36 x,y,z : reserved: transient objet denoted by a small letter
38 NAMING CONVENTIONS FOR CONSTRUCTORS
43 A: application to vector
52 n: native type annotation
54 NAMING CONVENTIONS FOR TRANSFORMATIONS AND RELATED FORMS
56 - prefix and first letter
58 b: bi contex-sensitive for local environments
59 c: contex-sensitive for terms
60 f: context-freee for closures
61 l: sn contex-sensitive for local environments
62 r: dx contex-sensitive for local environments
63 s: stratified (prefix)
64 t: context-free for terms
70 p: reflexive parallel transformation
71 q: sequential transformation
73 s: strongly normalizing form
79 d: decomposed rt-reduction
80 e: decomposed rt-conversion
81 q: restricted reduction
85 w: reserved for generic pointwise extension
89 - forth letter (if present)
91 c: proper single step (general) (successor)
92 e: reflexive transitive closure to normal form (evaluation)
93 g: proper multiple step (general) (greater)
94 p: non-reflexive transitive closure (plus)
95 q: reflexive closure (question)
96 r: proper multiple step (restricted) (restricted)
97 s: reflexive transitive closure (star)
98 u: proper single step (restricted) (unit)
99 x: reserved for generic pointwise extension