Duplicated error when using placeholders in simpa
#5634
Labels
bug
Something isn't working
Comments
kmill
added a commit
to kmill/lean4
that referenced
this issue
Oct 8, 2024
Closes leanprover#5634. Before assigning the `using` clause expression to the goal, this adds a check that the expression has no new metavariables. It also admits the goal when we report new metavariables since asserting the term as a new hypothesis causes it to be linked to pre-existing goals, leading to "don't know how to synthesize placeholder" errors for them. We also throw in an occurs check immediately after elaboration to avoid some counterintuitive behavior with simp.
github-merge-queue bot
pushed a commit
that referenced
this issue
Oct 8, 2024
Closes #5634. Before assigning the simplified `using` clause expression to the goal, this adds a check that the expression has no new metavariables. It also adjusts how new hypotheses are added to the goal to prevent spurious "don't know how to synthesize placeholder" errors on that goal metavariable. We also throw in an occurs check immediately after elaboration to avoid some counterintuitive behavior when simplifying such a term closes the goal. Closes #4101. This also improves the type mismatch error message, showing the elaborated `using` clause rather than `h✝`: ```lean example : False := by simpa using (fun x : True => x) /- error: type mismatch, term fun x => x after simplification has type True : Prop but is expected to have type False : Prop -/ ```
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Prerequisites
Please put an X between the brackets as you perform the following steps:
https://github.com/leanprover/lean4/issues
Avoid dependencies to Mathlib or Batteries.
https://live.lean-lang.org/#project=lean-nightly
(You can also use the settings there to switch to “Lean nightly”)
Description
The following code
leads to two errors: one is the expected
don't know how to synthesize placeholder for argument 'a'on the underscore. However, additionally, on the entire first line of the proof, we get anotherdon't know how to synthesize placeholdererror (this time without reference to the argument).Steps to Reproduce
Expected behavior: Only one error on the underscore
Actual behavior: A second error on the
haveline.Versions
4.12.0-nightly-2024-10-03on live.lean-lang.orgImpact
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: