[Backport releases/v4.8.0] fix: rfl tactic error messsage when there are no goals - Githubissues

leanprover / lean4

Lean 4 programming language and theorem prover

https://lean-lang.org

Apache License 2.0

3.82k stars 325 forks source link

[Backport releases/v4.8.0] fix: rfl tactic error messsage when there are no goals #4068

Closed github-actions[bot] closed 1 week ago

github-actions[bot] commented 1 week ago

Backport 26a1b934c226c6aa923248804ba92c23f56c5115 from #4067.