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 P : relocation environment
14 Q : elimination predicate
15 R : generic predicate/relation
18 X,Y,Z : reserved: transient objet denoted by a capital letter
20 a : applicability condition (true = restricted, false = general)
21 b : local dropping kind parameter (true = restricted, false = general)
22 c : rt-reduction count parameter
24 e : reserved: future use (\lambda\delta 3)
25 f,g : local reference transforming map
26 h : sort hierarchy parameter
27 i,j : local reference depth (de Bruijn's)
28 k,l : global reference level
30 o : sort degree parameter (origin)
35 v,w : 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
49 b: generic binder with one argument
51 f: generic flat with one argument
52 i: generic binder for local environments
54 n: native type annotation
55 u: generic binder with zero argument
58 NAMING CONVENTIONS FOR TRANSFORMATIONS AND RELATED FORMS
60 - prefix and first letter
62 b: bi contex-sensitive for local environments
63 c: contex-sensitive for terms
64 f: context-freee for closures
65 l: sn contex-sensitive for local environments
66 r: dx contex-sensitive for local environments
67 s: stratified (prefix)
68 t: context-free for terms
72 e: reserved for generic entrywise extension
75 p: reflexive parallel transformation
76 q: sequential transformation
78 s: strongly normalizing form
84 d: decomposed rt-reduction
85 e: decomposed rt-conversion
86 g: counted rt-transition (generic)
87 m: semi-counted rt-transition (mixed)
88 q: restricted reduction
92 w: reserved for generic pointwise extension
93 x: uncounted rt-transition (extended)
96 - forth letter (if present)
98 c: proper single step (general) (successor)
99 e: reflexive transitive closure to normal form (evaluation)
100 g: proper multiple step (general) (greater)
101 p: non-reflexive transitive closure (plus)
102 q: reflexive closure (question)
103 r: proper multiple step (restricted) (restricted)
104 s: reflexive transitive closure (star)
105 u: proper single step (restricted) (unit)