From 986de330971f653b6068c69615b17ce9c1273733 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 20 Jun 2022 09:57:14 -0700 Subject: [PATCH] fix: fixes #1230 --- src/Init/Tactics.lean | 4 ++-- tests/lean/run/1230.lean | 3 +++ 2 files changed, 5 insertions(+), 2 deletions(-) create mode 100644 tests/lean/run/1230.lean diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean index 46ad7afbcf..b959d68fcf 100644 --- a/src/Init/Tactics.lean +++ b/src/Init/Tactics.lean @@ -170,9 +170,9 @@ macro "rfl'" : tactic => `(set_option smartUnfolding false in with_unfolding_all syntax (name := ac_refl) "ac_refl " : tactic /-- `admit` is a shorthand for `exact sorry`. -/ -macro "admit" : tactic => `(exact sorry) +macro "admit" : tactic => `(exact @sorryAx _ false) /-- The `sorry` tactic is a shorthand for `exact sorry`. -/ -macro "sorry" : tactic => `(exact sorry) +macro "sorry" : tactic => `(exact @sorryAx _ false) /-- `infer_instance` is an abbreviation for `exact inferInstance` -/ macro "infer_instance" : tactic => `(exact inferInstance) diff --git a/tests/lean/run/1230.lean b/tests/lean/run/1230.lean new file mode 100644 index 0000000000..61ab14a5f3 --- /dev/null +++ b/tests/lean/run/1230.lean @@ -0,0 +1,3 @@ +example: ∀ {t}, 0 ≤ t := by + have : True := trivial + sorry