Lean4
/-- This is the definition of regular expressions. The names used here is to mirror the definition
of a Kleene algebra (https://en.wikipedia.org/wiki/Kleene_algebra).
* `0` (`zero`) matches nothing
* `1` (`epsilon`) matches only the empty string
* `char a` matches only the string 'a'
* `star P` matches any finite concatenation of strings which match `P`
* `P + Q` (`plus P Q`) matches anything which match `P` or `Q`
* `P * Q` (`comp P Q`) matches `x ++ y` if `x` matches `P` and `y` matches `Q`
-/
inductive RegularExpression (α : Type u) : Type u
| zero : RegularExpression α
| epsilon : RegularExpression α
| char : α → RegularExpression α
| plus : RegularExpression α → RegularExpression α → RegularExpression α
| comp : RegularExpression α → RegularExpression α → RegularExpression α
| star : RegularExpression α → RegularExpression α
