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

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

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

def Lean.Elab.Tactic.Conv.congrFunN (mvarId : MVarId) : MetaM MVarId

Implementation of arg 0.

def Lean.Elab.Tactic.Conv.congrArgForall (tacticName : String) (domain : Bool) (mvarId : MVarId) (lhs rhs : Expr) : MetaM (List MVarId)

Implements arg for foralls. If domain is true, accesses the domain, otherwise accesses the codomain.

def Lean.Elab.Tactic.Conv.congrArgN (tacticName : String) (mvarId : MVarId) (i : Int) (explicit : Bool) : MetaM (List MVarId)

Implementation of arg i.

def Lean.Elab.Tactic.Conv.congrArgN.applyArgs (tacticName : String) (explicit : Bool) (f : Expr) (xs : Array Expr) (i : Int) : MetaM (Expr × Array Expr)

def Lean.Elab.Tactic.Conv.evalArg (tacticName : String) (i : Int) (explicit : Bool) : TacticM Unit

def Lean.Elab.Tactic.Conv.elabArg : Tactic

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

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

def Lean.Elab.Tactic.Conv.evalFun : Tactic

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

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

def Lean.Elab.Tactic.Conv.evalEnter : Tactic