LR(k) languages are context-free

An LR(k) grammar is, by definition, one of the repository's context-free grammars (CF_grammar) carrying an extra determinacy property, so the language it generates is context-free. This file records that inclusion at the language-class level.

Main results

• is_CF_of_is_LRk — every LR(k) language is context-free
• is_CF_of_is_LR — every LR language is context-free
• LR_subclass_CF — LR ⊆ CF

theorem is_CF_of_is_LRk {T : Type} {k : ℕ} {L : Language T} (h : is_LRk k L) : is_CF L

Every LR(k) language is context-free.

theorem is_CF_of_is_LR {T : Type} {L : Language T} (h : is_LR L) : is_CF L

Every LR language is context-free.

theorem LR_subclass_CF {T : Type} : LR ⊆ CF

The class of LR languages is contained in the class of context-free languages.