You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
commit 6080e3dd5cc76d9f8807de19d6575f517ee11899
Author: Leonardo de Moura <leomoura@amazon.com>
Date: Tue Jul 2 15:42:47 2024 +0200
fix: enforce `isDefEqStuckEx` at `unstuckMVar` procedure (#4596)
Closes #2736
See comment at `ExprDefEq.lean` for explanation.
Side effects:
- Improved error messages in two tests.
- Had to improve `getSuccesses` procedure at `App.lean`. It now
discards candidates that contain postponed elaboration problems.
If it is too disruptive for Mathlib, we should try to discard the
ones that have postponed metavariables.
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: