  We formalized general (i.e., type-0) grammars using the Lean 3 proof
assistant. We defined basic notions of rewrite rules and of words derived by a
grammar, and used grammars to show closure of the class of type-0 languages
under four operations: union, reversal, concatenation, and the Kleene star. The
literature mostly focuses on Turing machine arguments, which are possibly more
difficult to formalize. For the Kleene star, we could not follow the literature
and came up with our own grammar-based construction.
