]> matita.cs.unibo.it Git - helm.git/blob - helm/coq-contribs/lambdadelta/web/basic_1_src.tbl
milestone update in basic_2
[helm.git] / helm / coq-contribs / lambdadelta / web / basic_1_src.tbl
1 name "basic_1_src"
2
3 table uri "static/coq/lambdadelta/basic_1/" ext ".txt" {
4    class "gray"
5    [ { "component" * } {
6         [ { "plane" * } {
7              [ "files" * ]
8           }
9         ]
10      }
11    ]
12    class "wine"
13    [ { "examples" * } {
14         [ { "terms with special features" * } {
15              [ @@"levels_ex0" + @@"ty3_ex1" + @@"nf2_ex2" * ]
16           }
17         ]
18      }
19    ]
20    class "magenta"
21    [ { "" * } {
22         [ { "" * } {
23              [ "" * ]
24           }
25         ]
26      }
27    ]
28 (*   
29    [ { "higher order dynamic typing" * } {
30         [ { "higher order native type assignment" * } {
31              [ "ntas ( ⦃?,?⦄ ⊢ ? :* ? )" "nta_lift" * ]
32           }
33         ]
34      }
35    ]
36 *)
37    class "prune"
38    [ { "dynamic typing" * } {
39         [ { "well-formed contexts" * } {
40              [ @@"wf3_defs" @@"wf3_props" * ]
41           }
42         ]
43         [ { "context ref. for native type assignment" * } {
44              [ @@"csubt_defs" @@"csubt_props" + @@"csubt_arity_props" * ]
45           }
46         ]
47         [ { "native type assignment" * } {
48              [ @@"ty3_defs" @@"ty3_props" + @@"ty3_gen" + @@"ty3_gen_context" + @@"ty3_gen_nf2" + @@"ty3_lift" + @@"ty3_subst0" + @@"ty3_arity_props" + @@"ty3_nf2_gen" + @@"ty3_sred" + @@"ty3_sred_props" + @@"ty3_dec" * ]
49           }
50         ]
51      }
52    ]
53    class "blue"
54    [ { "equivalence" * } {
55         [ { "context-sensitive equivalence" * } {
56              [ @@"pc3_defs" @@"pc3_props" + @@"pc3_gen" + @@"pc3_gen_context" + @@"pc3_subst0" * ]
57           }
58         ]
59         [ { "context-free equivalence" * } {
60              [ @@"pc1_defs" @@"pc1_props" * ]
61           }
62         ]
63      }
64    ]
65    class "sky"
66    [ { "" * } {
67         [ { "" * } {
68              [ "" * ]
69           }
70         ]
71      }
72    ]
73    class "cyan"
74    [ { "computation" * } {
75         [ { "context ref. for reducibility" * } {
76              [ @@"csubc_defs" @@"csubc_props" * ]
77           }
78         ]
79         [ { "reducibility" * } {
80              [ @@"sc3_defs" @@"sc3_props" + @@"sc3_arity" * ]
81           }
82         ]
83         [ { "strongly normalizing computation" * } {
84              [ @@"sn3_defs" @@"sn3_gen" + @@"sn3_props" * ]
85           }
86         ]
87         [ { "context-sensitive computation" * } {
88              [ @@"pr3_defs" @@"pr3_props" + @@"pr3_gen" + @@"pr3_gen_context" + @@"pr3_iso" + @@"pr3_subst1" + @@"pr3_confluence" * ]
89           }
90         ]
91         [ { "context-free computation" * } {
92              [ @@"pr1_defs" @@"pr1_props" + @@"pr1_confluence" * ]
93           }
94         ]
95      }
96    ]
97    class "water"
98    [ { "reduction" * } {
99         [ { "normal forms for context-sensitive reduction" * } {
100              [ @@"nf2_defs" @@"nf2_props" + @@"nf2_gen" + @@"nf2_dec" * ]
101           }
102         ]
103         [ { "context-sensitive reduction" * } {
104              [ @@"pr2_defs" @@"pr2_gen" + @@"pr2_gen_context" + @@"pr2_lift" + @@"pr2_subst1" + @@"pr2_confluence" * ]
105           }
106         ]
107         [ { "normal forms for context-free reduction" * } {
108              [ "" @@"nf0_dec" * ]
109           }
110         ]
111         [ { "context-free reduction" * } {
112              [ @@"wcpr0_defs" * ]
113              [ @@"pr0_defs" @@"pr0_gen" + @@"pr0_lift" + @@"pr0_subst0" + @@"pr0_subst1" + @@"pr0_confluence" * ]
114           }
115         ]
116      }
117    ]
118    class "green"
119    [ { "unfold" * } {
120         [ { "iterated static type assignment" * } {
121              [ @@"sty1_defs" @@"sty1_props" * ]
122           }
123         ]
124      }
125    ]
126    class "grass"
127    [ { "static typing" * } {
128         [ { "static type assignment" * } {
129              [ @@"sty0_defs" @@"sty0_props" * ]
130           }
131         ]
132         [ { "context ref. for binary arity assignment" * } {
133              [ @@"csuba_defs" @@"csuba_props" * ]
134           }
135         ]
136         [ { "binary arity assignment" * } {
137              [ @@"arity_defs" @@"arity_props" + @@"arity_gen" + @@"arity_subst0" + @@"arity_sred" * ]
138           }
139         ]
140         [ { "binary arity" * } {
141              [ @@"levels_defs" + @@"llt_defs" + @@"aprem_defs" * ]
142           }
143         ]
144         [ { "parameters" * } {
145              [ @@"parameter_defs" * ]
146           }
147         ]
148         [ { "basic context ref." * } {
149              [ @@"csubv_defs" * ]
150           }
151         ]
152      }
153    ]
154    class "yellow"
155    [ { "multiple substitution" * } {
156         [ { "iterated context slicing" * } {
157              [ @@"drop1_defs" @@"drop1_props" * ]
158           }
159         ]
160         [ { "generic term relocation" * } {
161              [ @@"lift1_defs" @@"lift1_props" * ]
162           }
163         ]
164      }
165    ]
166    class "orange"
167    [ { "substitution" * } {
168         [ { "ordinary substitution" * } {
169              [ @@"subst_defs" @@"subst_props" * ]
170              [ @@"csubst1_defs" @@"csubst1_props" * ]
171              [ @@"subst1_defs" @@"subst1_gen" + @@"subst1_lift" + @@"subst1_subst1" + @@"subst1_confluence" * ]
172           }
173         ]
174         [ { "normal forms for ordinary strict substitution" * } {
175              [ "" @@"dnf_dec" * ]
176           }
177         ]
178         [ { "ordinary strict substitution" * } {
179              [ @@"fsubst0_defs" * ]
180              [ @@"csubst0_defs" * ]
181              [ @@"subst0_defs" @@"subst0_gen" + @@"subst0_tlt" + @@"subst0_lift" + @@"subst0_subst0" + @@"subst0_confluence" * ]
182           }
183         ]
184         [ { "basic local env. slicing" * } {
185              [ @@"getl_defs" @@"getl_props" * ]
186              [ @@"drop_defs" @@"drop_props" * ]
187           }
188         ]
189         [ { "basic term relocation" * } {
190              [ @@"lift_defs" @@"lift_props" + @@"lift_gen" + @@"lift_tlt" * ]
191           }
192         ]
193      }
194    ]
195    class "red"
196    [ { "grammar" * } {
197         [ { "closures" * } {
198              [ @@"flt_defs" * ]
199           }
200         ]
201         [ { "contexts" * } {
202              [ @@"contexts_defs" + @@"clt_defs" + @@"ctail_defs" + @@"app_defs" + @@"cnt_defs" * ]
203           }
204         ]
205         [ { "terms" * } {
206              [ @@"tlist_defs" * ]
207              [ @@"terms_defs" + @@"tlt_defs" + @@"iso_defs" * ]
208           }
209         ]
210      }
211    ]
212 }
213
214 class "top"               { * }
215
216 class "capitalize italic" { 0 }
217
218 class "italic"            { 1 }