(6steps)
PrintForm
Definitions
mb
automata
2
Sections
GenAutomata
Doc
At:
member
dec
lookup
ds:Collection(dec()), x:Label, T:SimpleType. T
dec_lookup(ds;x)
mk_dec(x, T)
ds
By:
Unfold `dec_lookup` 0
THEN
RW ColMemberC 0
THEN
ExRepD
Generated subgoals:
1
1.
ds:
Collection(dec())
2.
x:
Label
3.
T:
SimpleType
4.
d:
dec()
5.
d
ds
6.
d.lbl =
x
7.
T = d.typ
mk_dec(x, T)
ds
2
1.
ds:
Collection(dec())
2.
x:
Label
3.
T:
SimpleType
4.
mk_dec(x, T)
ds
d:dec(). d
ds & d.lbl =
x & T = d.typ
About:
(6steps)
PrintForm
Definitions
mb
automata
2
Sections
GenAutomata
Doc