Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

fix: do not ban .. with a . on the next line #4768

Open
wants to merge 3 commits into
base: master
Choose a base branch
from
Open

fix: do not ban .. with a . on the next line #4768

wants to merge 3 commits into from

Conversation

eric-wieser
Copy link
Contributor

@eric-wieser eric-wieser commented Jul 17, 2024 •
edited
Loading

Without this change,

example : True := by
  refine' trivial ..
  . trivial

is a parse error.

@eric-wieser eric-wieser requested a review from Kha as a code owner July 17, 2024 01:16
@eric-wieser eric-wieser marked this pull request as draft July 17, 2024 01:16
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Jul 17, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

leanprover-community-mathlib4-bot commented Jul 17, 2024 •
edited
Loading

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 1a12f63f742a578a514536ef45cf9df0c9793af0 --onto 7aec6c9ae7a54935ada0df0b4cc1efafc2291007. (2024-07-17 01:32:53)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 1a12f63f742a578a514536ef45cf9df0c9793af0 --onto 647a5e94925791f6a16b629b6c16ffad60a7f478. (2024-08-05 21:35:26)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 1a12f63f742a578a514536ef45cf9df0c9793af0 --onto 9ce15fb0c61e3a1bee17fd81647ed4d02b4f6c6d. (2024-08-29 22:47:38)

@Kha
Copy link
Member

Kha commented Jul 19, 2024

Why is this a draft?

@eric-wieser
Copy link
Contributor Author

eric-wieser commented Jul 19, 2024 •
edited
Loading

It has no tests yet and the description implies it should be draft if I haven't filed an issue first.

@leodemoura leodemoura force-pushed the master branch 2 times, most recently from 32d60c5 to 696f70b Compare July 20, 2024 02:58
@leanprover-bot leanprover-bot added the P-medium We may work on this issue if we find the time label Jul 22, 2024
@eric-wieser
fix: do not ban .. with a . on the next line
bb66d4d 
Without this change,
```lean
example : True := by
  refine' trivial ..
  . trivial
```
is a parse error.
@eric-wieser eric-wieser marked this pull request as ready for review August 5, 2024 21:16
@eric-wieser
Copy link
Contributor Author

I've added the test from the description

@Kha
Copy link
Member

Kha commented Aug 8, 2024 •
edited
Loading

Thanks. Please add a module docstring to the test describing its purpose as mentioned in testing.md

@eric-wieser
Copy link
Contributor Author

Sorry for the delay, the docstring is now present.

@github-actions github-actions bot added the awaiting-review Waiting for someone to review the PR label Aug 31, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@Kha Kha Awaiting requested review from Kha Kha is a code owner

Assignees
No one assigned
Labels
awaiting-review Waiting for someone to review the PR P-medium We may work on this issue if we find the time toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
4 participants
@eric-wieser @leanprover-community-mathlib4-bot @Kha @leanprover-bot