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

chore: style

Browse source
This commit is contained in:
Leonardo de Moura 2022-06-10 18:27:43 -07:00
parent 033618ad5e
commit 8a8a8b5e48
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

@ -11,7 +11,7 @@ open Meta
/-- Returns a list of new congruence subgoals, which contains `none` for each argument with
forward dependencies. -/
private def congrApp (mvarId : MVarId) (lhs rhs : Expr) : MetaM (List $ Option MVarId) :=
private def congrApp (mvarId : MVarId) (lhs rhs : Expr) : MetaM (List (Option MVarId)) :=
-- TODO: add support for `[congr]` lemmas
lhs.withApp fun f args => do
let infos := (← getFunInfoNArgs f args.size).paramInfo
@ -55,21 +55,21 @@ def isImplies (e : Expr) : MetaM Bool :=
else
return false
def congr (mvarId : MVarId) : MetaM (List $ Option MVarId) :=
def congr (mvarId : MVarId) : MetaM (List (Option MVarId)) :=
withMVarContext mvarId do
let (lhs, rhs) ← getLhsRhsCore mvarId
let lhs := (← instantiateMVars lhs).consumeMData
if (← isImplies lhs) then
pure $ (← congrImplies mvarId).map Option.some
return (← congrImplies mvarId).map Option.some
else if lhs.isApp then
congrApp mvarId lhs rhs
else
throwError "invalid 'congr' conv tactic, application or implication expected{indentExpr lhs}"
@[builtinTactic Lean.Parser.Tactic.Conv.congr] def evalCongr : Tactic := fun _ => do
replaceMainGoal $ List.filterMap id (← congr (← getMainGoal))
replaceMainGoal <| List.filterMap id (← congr (← getMainGoal))
private def selectIdx (tacticName : String) (mvarIds : List $ Option MVarId) (i : Int) :
private def selectIdx (tacticName : String) (mvarIds : List (Option MVarId)) (i : Int) :
TacticM Unit := do
if i >= 0 then
let i := i.toNat