Definitions
GenAutomata
Sections
NuprlLIB
Doc
No mentions to report in GenAutomata
st_top
Def tTop == tree_leaf(inr(
))
Thm* tTop
SimpleType
tree_leaf
Def
tree_leaf(x) == inl(x)
Thm*
E,T:Type, x:E. tree_leaf(x)
tree_con(E;T)
Thm*
E:Type, x:E. tree_leaf(x)
Tree(E)
Syntax:
tTop
has structure:
st_top
About:
Definitions
GenAutomata
Sections
NuprlLIB
Doc