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
19 c : local dropping kind parameter (true = restricted, false = general)
21 e : reserved: future use (\lambda\delta 3)
22 f,g : local reference transforming map
23 h : sort hierarchy parameter
24 i,j : local reference depth (de Bruijn's)
25 k,l : global reference level
28 o : sort degree parameter
30 r : reduction kind parameter (true = ordinary, false = extended)
33 v,w : local reference position level (de Bruijn's) (RTM)
34 x,y,z : reserved: transient objet denoted by a small letter
36 NAMING CONVENTIONS FOR CONSTRUCTORS
41 A: application to vector
50 n: native type annotation
52 NAMING CONVENTIONS FOR TRANSFORMATIONS AND RELATED FORMS
54 - prefix and first letter
56 b: bi contex-sensitive for local environments
57 c: contex-sensitive for terms
58 f: context-freee for closures
59 l: sn contex-sensitive for local environments
60 r: dx contex-sensitive for local environments
61 s: stratified (prefix)
62 t: context-free for terms
66 e: reserved for generic entrywise extension
69 p: reflexive parallel transformation
70 q: sequential transformation
72 s: strongly normalizing form
78 d: decomposed rt-reduction
79 e: decomposed rt-conversion
80 q: restricted reduction
84 w: reserved for generic pointwise extension
88 - forth letter (if present)
90 c: proper single step (general) (successor)
91 e: reflexive transitive closure to normal form (evaluation)
92 g: proper multiple step (general) (greater)
93 p: non-reflexive transitive closure (plus)
94 q: reflexive closure (question)
95 r: proper multiple step (restricted) (restricted)
96 s: reflexive transitive closure (star)
97 u: proper single step (restricted) (unit)