Closed chrisflav closed 1 week ago
The new error message printed by the rfl tactic is also shown when rfl is used with no goals left.
rfl
example : 3 = 3 := by rfl rfl
This prints on the second rfl:
The rfl tactic failed. Possible reasons: The goal is not a reflexive relation (neither = nor a relation with a @[refl] lemma). The arguments of the relation are not equal. Try using the reflexivitiy lemma for your relation explicitly, e.g. exact Eq.rfl.
The rfl tactic failed. Possible reasons:
=
Try using the reflexivitiy lemma for your relation explicitly, e.g. exact Eq.rfl.
exact Eq.rfl
but should instead print
no goals to be solved
Expected behavior: Print "no goals to be solved" error message
Actual behavior: Standard rfl error message is shown.
4.8.0-rc1 Debian Bookworm / https://live.lean-lang.org
Add :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.
Prerequisites
Description
The new error message printed by the
rfl
tactic is also shown whenrfl
is used with no goals left.This prints on the second
rfl
:but should instead print
Steps to Reproduce
Expected behavior: Print "no goals to be solved" error message
Actual behavior: Standard
rfl
error message is shown.Versions
4.8.0-rc1 Debian Bookworm / https://live.lean-lang.org
Impact
Add :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.