def Lean.Elab.Tactic.Conv.congr (mvarId : Lean.MVarId) (addImplicitArgs : optParam Bool false) (nameSubgoals : optParam Bool true) : Lean.MetaM (List (Option Lean.MVarId))

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Tactic.Conv.evalCongr : Lean.Elab.Tactic.Tactic

Equations

• Lean.Elab.Tactic.Conv.evalCongr x = do let a ← Lean.Elab.Tactic.getMainGoal let a ← liftM (Lean.Elab.Tactic.Conv.congr a false true) Lean.Elab.Tactic.replaceMainGoal (List.filterMap id a)

def Lean.Elab.Tactic.Conv.evalSkip : Lean.Elab.Tactic.Tactic

Equations

• Lean.Elab.Tactic.Conv.evalSkip x = pure ()

def Lean.Elab.Tactic.Conv.evalLhs : Lean.Elab.Tactic.Tactic

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Tactic.Conv.evalRhs : Lean.Elab.Tactic.Tactic

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Tactic.Conv.evalArg : Lean.Elab.Tactic.Tactic

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Tactic.Conv.extLetBodyCongr? (mvarId : Lean.MVarId) (lhs : Lean.Expr) (rhs : Lean.Expr) : Lean.MetaM (Option Lean.MVarId)

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Tactic.Conv.evalExt : Lean.Elab.Tactic.Tactic

Equations

• One or more equations did not get rendered due to their size.