chore: upstream exfalso

2026-04-04 19:24:09 +00:00 · 2024-02-16 12:38:12 +11:00
1 changed files with 3 additions and 0 deletions
--- a/src/Init/Tactics.lean
+++ b/src/Init/Tactics.lean
@@ -201,6 +201,9 @@ and implicit parameters are also converted into new goals.
 -/
 syntax (name := refine') "refine' " term : tactic

+/-- `exfalso` converts a goal `⊢ tgt` into `⊢ False` by applying `False.elim`. -/
+macro "exfalso" : tactic => `(tactic| refine False.elim ?_)
+
 /--
 If the main goal's target type is an inductive type, `constructor` solves it with
 the first matching constructor, or else fails.