grammar 1 Sections AutomataTheory Doc

start Def S == inl(G.init)

Thm* V,T:Type, G:Grammar(V;T). S V+T

g_init Def g.init == 2of(g)

Thm* V,T:Type, g:Grammar(V;T). g.init V

pi2 Def 2of(t) == t.2

Thm* A:Type, B:(AType), p:a:AB(a). 2of(p) B(1of(p))

About:
!abstractionspreadalluniversefunction
productmemberinlunion