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

fix: match tactic should not trigger implicit lambdas

Browse source
This commit is contained in:
Sebastian Ullrich 2022-02-04 10:06:40 +01:00 • committed by Leonardo de Moura
parent 7fd76cd1b9
commit ae062c6ead
3 changed files with 27 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -63,7 +63,7 @@ private def mkAuxiliaryMatchTerm (parentTag : Name) (matchTac : Syntax) : MacroM
def evalMatch : Tactic := fun stx => do
let tag ← getMainTag
let (matchTerm, cases) ← liftMacroM <| mkAuxiliaryMatchTerm tag stx
let refineMatchTerm ← `(tactic| refine $matchTerm)
let refineMatchTerm ← `(tactic| refine no_implicit_lambda% $matchTerm)
let stxNew := mkNullNode (#[refineMatchTerm] ++ cases)
withMacroExpansion stx stxNew <| evalTactic stxNew

10
tests/lean/995.lean Normal file
View file

@ -0,0 +1,10 @@
example : ∀(x : Nat){h : x = x}, Nat := by
intro x
match x with
| 0 => _
| n + 1 => _
example (x : Nat) : ∀{h : x = x}, Nat := by
match x with
| 0 => _
| n + 1 => _

16
tests/lean/995.lean.expected.out Normal file
View file

@ -0,0 +1,16 @@
995.lean:1:40-5:14: error: unsolved goals
case match_1
x : Nat
⊢ {h : 0 = 0} → Nat
case match_2
x n : Nat
⊢ {h : n + 1 = n + 1} → Nat
995.lean:7:41-10:14: error: unsolved goals
case match_1
x : Nat
⊢ {h : 0 = 0} → Nat
case match_2
x n : Nat
⊢ {h : n + 1 = n + 1} → Nat