(2steps) PrintForm Definitions Lemmas mb automata 3 Sections GenAutomata Doc

At: record select wf decls mng2 1

1. ds: Collection(dec())
2. rho: Decl
3. s: l:Label[[ds]] rho(l)
4. x: Label
5. t: SimpleType
6. t dec_lookup(ds;x)

mk_dec(x, t) ds

By: RWW "member_dec_lookup" -1

Generated subgoals:

None


About:
applyfunction

(2steps) PrintForm Definitions Lemmas mb automata 3 Sections GenAutomata Doc