max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: fixes #1230

Browse source
This commit is contained in:
Leonardo de Moura 2022-06-20 09:57:14 -07:00
parent b6f251bcd3
commit 986de33097
2 changed files with 5 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Init/Tactics.lean
View file

@ -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)

3
tests/lean/run/1230.lean Normal file
View file

@ -0,0 +1,3 @@
example: ∀ {t}, 0 ≤ t := by
have : True := trivial
sorry