Mathlib Map

Theorems · Inductive type · computer science

ContextFreeGrammar

Type u_1 → Type (max 1 u_1)

Context-free grammar that generates words over the alphabet T (a type of terminals).

Defined in
Mathlib.Computability.ContextFreeGrammar
Cited by
39 results in Mathlib
Foundations
Depth 0 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

ContextFreeGrammar.NT · cited by 30ContextFreeGrammar.NTContextFreeGrammar.Derives · cited by 19ContextFreeGrammar.DerivesContextFreeGrammar.reverse · cited by 19ContextFreeGrammar.reverseContextFreeGrammar.Produces · cited by 17ContextFreeGrammar.Produc…ContextFreeGrammar.rules · cited by 9ContextFreeGrammar.rulesContextFreeGrammar.initial · cited by 7ContextFreeGrammar.initialContextFreeGrammar.language · cited by 4ContextFreeGrammar.langua…Language.IsContextFree · cited by 3Language.IsContextFreeContextFreeGrammar.Derives.trans_produces · cited by 3Derives.trans_producesContextFreeGrammar.Generates · cited by 3ContextFreeGrammar.Genera…ContextFreeGrammar.Derives.trans · cited by 2Derives.transContextFreeGrammar.Produces.single · cited by 2Produces.singleLanguage.IsContextFree.reverse · cited by 2IsContextFree.reverseContextFreeGrammar.reverse_bijective · cited by 2ContextFreeGrammar.revers…ContextFreeGrammar.reverse_reverse · cited by 2ContextFreeGrammar.revers…ContextFreeGrammarCITED BYCITES

Cites0

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Nothing in Mathlib beyond the foundations.

Cited by54

Results whose statement or proof uses this declaration.