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

fix: specialize

Browse source
This commit is contained in:
Leonardo de Moura 2021-09-11 19:52:51 -07:00
parent 218b9c87b0
commit bbe6d37109
2 changed files with 12 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -101,7 +101,7 @@ def refineCore (stx : Syntax) (tagSuffix : Name) (allowNaturalHoles : Bool) : Ta
@[builtinTactic «specialize»] def evalSpecialize : Tactic := fun stx => withMainContext do
match stx with
| `(tactic| specialize $e:term) =>
let (e, mvarIds') ← elabTermWithHoles e (← getMainTarget) `specialize (allowNaturalHoles := true)
let (e, mvarIds') ← elabTermWithHoles e none `specialize (allowNaturalHoles := true)
let h := e.getAppFn
if h.isFVar then
let localDecl ← getLocalDecl h.fvarId!

11
tests/lean/run/specialize2.lean Normal file
View file

@ -0,0 +1,11 @@
example : (p → q → False) ↔ (¬ p ∨ ¬ q) := by
apply Iff.intro
. intro h
byCases hp:p <;> byCases hq:q
. specialize h hp hq; contradiction
. exact Or.inr hq
. exact Or.inl hp
. exact Or.inr hq
. intro
| Or.inl hnp => intros; contradiction
| Or.inr hnq => intros; contradiction