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

feat: upstream false_or_by_contra tests (#3947)

Browse source 
And fix broken `builtin_tactic` attribute.
This commit is contained in:
Kim Morrison 2024-04-19 07:30:51 +02:00 • committed by GitHub
parent d1a42aae2a
commit d6474135ba
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Elab/Tactic/FalseOrByContra.lean
View file

@ -58,7 +58,7 @@ partial def falseOrByContra (g : MVarId) (useClassical : Option Bool := none) :
let [g] ← g.applyConst ``False.elim | panic! "expected one sugoal"
pure g
@[builtin_tactic falseOrByContra]
@[builtin_tactic Lean.Parser.Tactic.falseOrByContra]
def elabFalseOrByContra : Tactic
| `(tactic| false_or_by_contra) => do liftMetaTactic1 (falseOrByContra ·)
| _ => no_error_if_unused% throwUnsupportedSyntax