mb label Sections GenAutomata Doc

Def ||as|| == Case of as; nil 0 ; a.as' ||as'||+1 (recursive)

is mentioned

In prior sections: list 1 mb list 1

Try larger context: GenAutomata

mb label Sections GenAutomata Doc