How the context-free languages are characterized by automata and by Mathlib.

Table of contents