Documentation

Lean.Elab.Tactic.Conv.Congr

def Lean.Elab.Tactic.Conv.isImplies (e : Lean.Expr) :

Lean.MetaM Bool

Equations

Lean.Elab.Tactic.Conv.isImplies e = if Lean.Expr.isArrow e = true then Lean.Meta.isProp (Lean.Expr.bindingDomain! e) <&&> Lean.Meta.isProp (Lean.Expr.bindingBody! e) else pure false

def Lean.Elab.Tactic.Conv.congr (mvarId : Lean.MVarId) (addImplicitArgs : optParam Bool false) :

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) Lean.Elab.Tactic.replaceMainGoal (List.filterMap id a)

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.