Indexed Languages

This file defines the class of indexed languages via indexed grammars.

Main declarations

• is_Indexed
• Indexed

def is_Indexed {T : Type} (L : Language T) : Prop

Predicate that a language is an indexed language.

Equations

• is_Indexed L = ∃ (g : IndexedGrammar T), g.Language = L

def Indexed {T : Type} : Set (Language T)

The class of indexed languages.

Equations

• Indexed = setOf is_Indexed