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

fix: missing withMainMVarContext

Browse source
This commit is contained in:
Leonardo de Moura 2020-10-26 11:35:54 -07:00
parent c55a65fe00
commit 40f99327e9
2 changed files with 7 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -195,7 +195,7 @@ private def getRecInfoDefault (major : Expr) (withAlts : Syntax) (allowMissingAl
withAlts : Parser := optional (" with " >> inductionAlts)
usingRec : Parser := optional (" using " >> ident)
``` -/
private def getRecInfo (stx : Syntax) (major : Expr) : TacticM RecInfo := withRef stx do
private def getRecInfo (stx : Syntax) (major : Expr) : TacticM RecInfo := withRef stx $ withMainMVarContext do
let usingRecStx := stx[2]
let withAlts := stx[4]
if usingRecStx.isNone then

6
tests/lean/run/inductionTacticBug.lean Normal file
View file

@ -0,0 +1,6 @@
def ex {α} : Subsingleton (Squash α) := Subsingleton.intro $ by
intro a b
induction a using Squash.ind
induction b using Squash.ind
apply Quot.sound
exact trivial