[Merged by Bors] - feat(Computability): define Language.IsRegular#13554
[Merged by Bors] - feat(Computability): define Language.IsRegular#13554
Language.IsRegular#13554Conversation
|
Please check that the universe levels are done correctly! |
|
We really need to move |
https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Regular/Basic.html#IsRegular Yeah! |
|
Can we proceed now regardless? |
PR summary ce152007beImport changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diff
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 |
|
|
||
| universe u v | ||
|
|
||
| open Computability |
There was a problem hiding this comment.
Actually the standard is to have
open ...
open scoped ...
universe ...
variable ...
It's important to have open .../open scoped ... before variable ... because the latter might use some names or notations only accessible in a namespace, and universe is a very close cousin of variable so should stay next to it
There was a problem hiding this comment.
OK, then it should probably make sense to replace
def Language.IsRegular {T : Type u}
by
def Language.IsRegular {T : Type*}
right?
There was a problem hiding this comment.
However, I am not sure the existentially-quantified type will accept Type* in place of Type v.
There was a problem hiding this comment.
All I'm saying is that you should revert the change I've commented on
There was a problem hiding this comment.
Did you take into account that the universes are used outside of the section as well as inside it?
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
|
maintainer merge |
|
🚀 Pull request has been placed on the maintainer queue by YaelDillies. |
|
bors merge |
This PR defines a predicate `Language.IsRegular` in a similar way `Language.IsContextFree` is defined.
|
This PR was included in a batch that was canceled, it will be automatically retried |
This PR defines a predicate `Language.IsRegular` in a similar way `Language.IsContextFree` is defined.
|
This PR was included in a batch that was canceled, it will be automatically retried |
|
Canceled. |
|
FYI, I didn't have any conflict and, after the merge, the file |
|
bors merge |
|
🔒 Permission denied Existing reviewers: click here to make madvorak a reviewer |
|
bors merge |
This PR defines a predicate `Language.IsRegular` in a similar way `Language.IsContextFree` is defined.
|
Pull request successfully merged into master. Build succeeded: |
Language.IsRegularLanguage.IsRegular
…age.IsContextFree` for consistency with #13554
This PR defines a predicate `Language.IsRegular` in a similar way `Language.IsContextFree` is defined.
This PR defines a predicate `Language.IsRegular` in a similar way `Language.IsContextFree` is defined.
This PR defines a predicate `Language.IsRegular` in a similar way `Language.IsContextFree` is defined.
This PR defines a predicate
Language.IsRegularin a similar wayLanguage.IsContextFreeis defined.