The singleton-word language {w}

The language containing exactly one fixed word w. This generalizes Langlib.Examples.EmptyWord (emptyWordLanguage T = singletonWordLanguage ([] : List T)).

It is regular (singletonWordLanguage_isRegular), and hence — being at the bottom of the Chomsky hierarchy — a member of every language class; those corollaries live in the Examples/SingletonWord.lean file of each class hierarchy.

def singletonWordLanguage {T : Type} (w : List T) : Language T

The language containing exactly the word w.

Equations

• singletonWordLanguage w = {w}