mb
automata
3
Sections
GenAutomata
Doc
Def
Case eq(x) = > body(x) cont(x1,z) == InjCase(x1; x2. body(x2); _. cont(z,z))
is mentioned by
Def
tc(r;ds;da;de) == Case(r.name) Case eq(Q) = > ||r.args|| = 2 & Q
term_types(ds;da;de;r.args[0]) & Q
term_types(ds;da;de;r.args[1]) Case R = > ||de.rel(R)|| = ||r.args||
& (
i:
. i < ||r.args||
(de.rel(R))[i]
term_types(ds;da;de;r.args[i])) Default = > False
[tc]
In prior sections:
mb
automata
1
mb
automata
2
Try larger context:
GenAutomata
mb
automata
3
Sections
GenAutomata
Doc