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

fix: extCore

Browse source
This commit is contained in:
Leonardo de Moura 2022-06-22 19:40:06 -07:00
parent a84b9b2e7b
commit 108bc4c27f
1 changed files with 5 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/Lean/Elab/Tactic/Conv/Congr.lean
View file

@ -139,20 +139,20 @@ private def extCore (mvarId : MVarId) (userName? : Option Name) : MetaM MVarId :
withMVarContext mvarId do
let userNames := if let some userName := userName? then [userName] else []
let (lhs, rhs) ← getLhsRhsCore mvarId
let lhs := (← instantiateMVars lhs).consumeMDataAndTypeAnnotations
let goForall (mvarId : MVarId) := do
let lhs ← instantiateMVars lhs
if lhs.isForall then
let [mvarId, _] ← apply mvarId (← mkConstWithFreshMVarLevels ``forall_congr) | throwError "'apply forall_congr' unexpected result"
let (_, mvarId) ← introN mvarId 1 userNames
markAsConvGoal mvarId
if lhs.isForall then
goForall mvarId
else if let some mvarId ← extLetBodyCongr? mvarId lhs rhs then
return mvarId
else
let lhsType ← whnfD (← inferType lhs)
unless lhsType.isForall do
throwError "invalid 'ext' conv tactic, function or arrow expected{indentD m!"{lhs} : {lhsType}"}"
goForall mvarId
let [mvarId] ← apply mvarId (← mkConstWithFreshMVarLevels ``funext) | throwError "'apply funext' unexpected result"
let (_, mvarId) ← introN mvarId 1 userNames
markAsConvGoal mvarId
private def ext (userName? : Option Name) : TacticM Unit := do
replaceMainGoal [← extCore (← getMainGoal) userName?]