action sets Sections AutomataTheory Doc

Def (n)! == if n=0 1 else n(n-1)! fi (recursive)

Thm* (0)! = 1 ex1_of_factorial