fix: rfl tactic error messsage when there are no goals

leanprover / lean4

Lean 4 programming language and theorem prover

https://lean-lang.org

Apache License 2.0

3.82k stars 325 forks source link

Closed nomeata closed 2 weeks ago

nomeata commented 2 weeks ago

fixes #4063

leanprover-community-mathlib4-bot commented 2 weeks ago

Mathlib CI status (docs):

❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 93d7afb00a9acb6ef0648cc2aeef798ca08d6ea9 --onto 00cf5771f31e7de7f6ab3089cb4b9ffa606a35ed. (2024-05-05 09:48:18)