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

fix: allow mkElimApp to assign new goals when solving typing constraints

Browse source
This commit is contained in:
Leonardo de Moura 2022-02-02 13:19:23 -08:00
parent 65e1fc1211
commit 4fe56d2a9d
1 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -116,7 +116,7 @@ partial def mkElimApp (elimName : Name) (elimInfo : ElimInfo) (targets : Array E
throwError "insufficient number of targets for '{elimName}'"
let target := ctx.targets[s.targetPos]
let expectedType ← getArgExpectedType
let target ← Term.ensureHasType expectedType target
let target ← withConfig (fun cfg => { cfg with assignSyntheticOpaque := true }) do Term.ensureHasType expectedType target
modify fun s => { s with targetPos := s.targetPos + 1 }
addNewArg target
else match c.binderInfo with
@ -150,7 +150,8 @@ partial def mkElimApp (elimName : Name) (elimInfo : ElimInfo) (targets : Array E
catch _ =>
setMVarKind mvarId MetavarKind.syntheticOpaque
others := others.push mvarId
return { elimApp := (← instantiateMVars s.f), alts := s.alts, others := others }
let alts ← s.alts.filterM fun alt => return !(← isExprMVarAssigned alt.2)
return { elimApp := (← instantiateMVars s.f), alts, others := others }
/- Given a goal `... targets ... |- C[targets]` associated with `mvarId`, assign
`motiveArg := fun targets => C[targets]` -/