Commit 2023-10-13 12:52 faa8dc9b

View on Github →

feat(Computability/CFG): define context-free grammars (#6385)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Computability/ContextFreeGrammar.lean

added theorem ContextFreeGrammar.Derives.eq_or_head

added theorem ContextFreeGrammar.Derives.eq_or_tail

added theorem ContextFreeGrammar.Derives.refl

added theorem ContextFreeGrammar.Derives.trans

added theorem ContextFreeGrammar.Derives.trans_produces

added def ContextFreeGrammar.Generates

added theorem ContextFreeGrammar.Produces.single

added theorem ContextFreeGrammar.Produces.trans_derives

added def ContextFreeGrammar.Produces

added def ContextFreeGrammar.language

added theorem ContextFreeGrammar.mem_language_iff

added structure ContextFreeGrammar.{uN,uT}

added theorem ContextFreeRule.Rewrites.exists_parts

added inductive ContextFreeRule.Rewrites

added theorem ContextFreeRule.rewrites_iff

added theorem ContextFreeRule.rewrites_of_exists_parts

added structure ContextFreeRule

Modified Mathlib/Computability/Language.lean

added inductive Symbol