PrintForm
Definitions
grammar
1
Sections
AutomataTheory
Doc
At:
directly
derive
wf
V,T:Type, G:Grammar(V;T).
(V+T)*
(V+T)*
Prop
By:
Unfold `directly_derive` 0
THEN
BackThru Thm*
T:Type, l:(T List
). l
T*
Generated subgoals:
None
About:
V,T:Type, G:Grammar(V;T). 
(V+T)*
(V+T)*PropT:Type, l:(T List
). l T*
