We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
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
calc
Although example : 3 + 9 = 12 := rfl works, the following code
example : 3 + 9 = 12 := rfl
example : 3 + 9 = 12 := calc 3 + 9 = 12 := rfl
fails with
type mismatch rfl has type 3 + 9 = 3 + 9 : Prop but is expected to have type 3 + 9 = 12 : Prop
Replacing rfl with by rfl or by exact rfl above makes it work, but I think it shouldn't be necessary.
rfl
by rfl
by exact rfl
Phil Wadler encountered this issue while porting his "Programming Language Foundations in Agda" book to Lean: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Debugging.20an.20issue.20with.20calc.20mode
This is a regression pointed out by Wadler after upgrading from an old nightly. I bisected it and it works on the 2023-01-05 nightly and fails on the 2023-01-06 one. According to https://github.com/leanprover/lean4-nightly/releases/tag/nightly-2023-01-06 this points to fedf235, but see also 474f1a4 where this was worked around for the show tactic.
show
In particular, plfa/plfl@a4684b2 contains three more calc uses which now require type ascriptions (and didn't need them before fedf235).
Lean 4.3.0-rc2 on Linux
Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.
The text was updated successfully, but these errors were encountered:
No branches or pull requests
Prerequisites
Description
Although
example : 3 + 9 = 12 := rfl
works, the following codefails with
Replacing
rfl
withby rfl
orby exact rfl
above makes it work, but I think it shouldn't be necessary.Context
Phil Wadler encountered this issue while porting his "Programming Language Foundations in Agda" book to Lean: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Debugging.20an.20issue.20with.20calc.20mode
This is a regression pointed out by Wadler after upgrading from an old nightly. I bisected it and it works on the 2023-01-05 nightly and fails on the 2023-01-06 one. According to https://github.com/leanprover/lean4-nightly/releases/tag/nightly-2023-01-06 this points to fedf235, but see also 474f1a4 where this was worked around for the
show
tactic.In particular, plfa/plfl@a4684b2 contains three more
calc
uses which now require type ascriptions (and didn't need them before fedf235).Versions
Lean 4.3.0-rc2 on Linux
Impact
Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.
The text was updated successfully, but these errors were encountered: