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

Equations

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

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

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

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

Implementation of arg 0.

Equations

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

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

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

Equations

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

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

Implementation of arg i.

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Lean.Elab.Tactic.Conv.evalLhs x = Lean.Elab.Tactic.Conv.evalArg "lhs" (-2) false

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

Equations

• Lean.Elab.Tactic.Conv.evalRhs x = Lean.Elab.Tactic.Conv.evalArg "rhs" (-1) false

def Lean.Elab.Tactic.Conv.evalFun : 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.
• Lean.Elab.Tactic.Conv.extLetBodyCongr? mvarId lhs rhs = pure none

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

Equations

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

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

Equations

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