mb hybrid Sections GenAutomata Doc

Def R^n == if n=0 x,y. x = y T else x,y. z:T. (x R z) & (z R^n-1 y) fi (recursive)

is mentioned

In prior sections: mb nat mb list 1

Try larger context: GenAutomata

mb hybrid Sections GenAutomata Doc