(7steps) PrintForm Definitions mb automata 3 Sections GenAutomata Doc

At: decls mng subtype 1 1 1
1. ds: Collection(dec())
2. rho: Decl
3. x: Label
4. y: d:{d:dec()| d ds }. [[d]] rho(x)
5. a: SimpleType
6. mk_dec(x, a) ds

mk_dec(x, a) {d:dec()| d ds }
By: Analyze
Generated subgoals:

None

About:
setisectapplymember

(7steps) PrintForm Definitions mb automata 3 Sections GenAutomata Doc