Commit 2023-12-22 14:46 623cc31f

View on Github →

feat(Computability/ContextFreeGrammar): derivations with prefix or postfix (#8630)

Estimated changes

Modified Mathlib/Computability/ContextFreeGrammar.lean

added theorem ContextFreeGrammar.Derives.append_left

added theorem ContextFreeGrammar.Derives.append_right

added theorem ContextFreeGrammar.Produces.append_left

added theorem ContextFreeGrammar.Produces.append_right

added theorem ContextFreeRule.Rewrites.append_left

added theorem ContextFreeRule.Rewrites.append_right