mb
automata
4
Sections
GenAutomata
Doc
Def
ioa_all(I; i.A(i)) == mk_ioa(
i:I. A(i).ds,
i:I. A(i).da,
i:I. A(i).init,
i:I. A(i).pre,
i:I. A(i).eff,
i:I. A(i).frame)
is mentioned by
Thm*
A:(I
ioa{i:l}()), rho:Decl, de:sig(), e:{[[de]] rho}, s:(
[[ioa_all(I; i.A(i)).da]] rho), i:I. s
[[A(i)]] rho de e.action
[ioa_all_mng_action]
Thm*
A:(I
ioa{i:l}()), rho:Decl, de:sig(), e:{[[de]] rho}, s:{[[ioa_all(I; i.A(i)).ds]] rho}, i:I. s
[[A(i)]] rho de e.state
[ioa_all_mng_state]
Try larger context:
GenAutomata
mb
automata
4
Sections
GenAutomata
Doc