mb automata 4 Sections GenAutomata Doc

Def tc_smt(s;ds;da;de) == mk_dec(s.lbl, s.typ) ds & s.typ term_types(ds;da;de;s.term)

is mentioned by

Def tc_eff(ef;ds;de) == tc_smt(ef.smt;ds; < ef.typ > ;de)[tc_eff]

Try larger context: GenAutomata

mb automata 4 Sections GenAutomata Doc