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

fix: refineCore

Browse source 
closes #269
This commit is contained in:
Leonardo de Moura 2021-01-15 17:03:40 -08:00
parent 58d51bc764
commit dcc2283426
2 changed files with 16 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

@ -63,7 +63,7 @@ def refineCore (stx : Syntax) (tagSuffix : Name) (allowNaturalHoles : Bool) : Ta
let decl ← getMVarDecl g
let (val, gs') ← elabTermWithHoles stx decl.type tagSuffix allowNaturalHoles
assignExprMVar g val
setGoals (gs ++ gs')
setGoals (gs' ++ gs)
@[builtinTactic «refine»] def evalRefine : Tactic := fun stx =>
match stx with

15
tests/lean/run/269.lean Normal file
View file

@ -0,0 +1,15 @@
theorem haveWithSubgoals {a b : α} : a = b ↔ b = a := by
apply Iff.intro
intro h
have h' := h.symm
exact h'
intro h
exact h.symm
theorem haveWithSubgoals2 {a b : α} : a = b ↔ b = a := by {
apply Iff.intro;
intro h;
have h' := h.symm;
exact h';
intro h; exact h.symm;
}