[Merged by Bors] - chore(Computability/ContextFreeGrammar): change the definition `Langu…#16268
[Merged by Bors] - chore(Computability/ContextFreeGrammar): change the definition `Langu…#16268
Conversation
…age.IsContextFree` for consistency with #13554
PR summary 9ab38f61d1Import changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diffNo declarations were harmed in the making of this PR! 🐙 You can run this locally as follows## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for |
|
🚀 Pull request has been placed on the maintainer queue by YaelDillies. |
| ∃ g : ContextFreeGrammar.{0} T, g.language = L | ||
|
|
||
| proof_wanted Language.isContextFree_iff {L : Language T} : | ||
| L.IsContextFree ↔ ∃ g : ContextFreeGrammar.{uN} T, g.language = L |
There was a problem hiding this comment.
Is this true? Can't you show that some simple language in Type 3 can't be IsContextFree in the sense of the new definition by cardinality reasons? Or do we require [Fintype _] somewhere along the path? UPD: ignore this, we can't reach more than countably many words, because we use a list of rules and a unique initial element.
|
Thanks! 🎉 |
|
This PR was included in a batch that was canceled, it will be automatically retried |
|
Pull request successfully merged into master. Build succeeded: |
…age.IsContextFree` for consistency with #13554