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