Documentation

Lean.Elab.Tactic.Conv.Basic

source
def Lean.Elab.Tactic.Conv.mkConvGoalFor (lhs : Lean.Expr) :
Lean.MetaM (Lean.Expr × Lean.Expr)
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.Conv.markAsConvGoal (mvarId : Lean.MVarId) :
Lean.MetaM Lean.MVarId
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.Conv.convert (lhs : Lean.Expr) (conv : Lean.Elab.Tactic.TacticM Unit) :
Lean.Elab.Tactic.TacticM (Lean.Expr × Lean.Expr)
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.Conv.getLhsRhsCore (mvarId : Lean.MVarId) :
Lean.MetaM (Lean.Expr × Lean.Expr)
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.Conv.getLhsRhs:
Lean.Elab.Tactic.TacticM (Lean.Expr × Lean.Expr)
Equations
source
def Lean.Elab.Tactic.Conv.getLhs:
Lean.Elab.Tactic.TacticM Lean.Expr
Equations
source
def Lean.Elab.Tactic.Conv.getRhs:
Lean.Elab.Tactic.TacticM Lean.Expr
Equations
source
def Lean.Elab.Tactic.Conv.updateLhs (lhs' : Lean.Expr) (h : Lean.Expr) :
Lean.Elab.Tactic.TacticM Unit

⊢ lhs = rhs ~~> ⊢ lhs' = rhs using h : lhs = lhs'.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.Conv.changeLhs (lhs' : Lean.Expr) :
Lean.Elab.Tactic.TacticM Unit

Replace lhs with the definitionally equal lhs'.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.Conv.evalWhnf:
Lean.Elab.Tactic.Tactic
Equations
source
def Lean.Elab.Tactic.Conv.evalReduce:
Lean.Elab.Tactic.Tactic
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.Conv.evalZeta:
Lean.Elab.Tactic.Tactic
Equations
source
def Lean.Elab.Tactic.Conv.evalConvSeq1Indented:
Lean.Elab.Tactic.Tactic
Equations
source
def Lean.Elab.Tactic.Conv.evalConvSeqBracketed:
Lean.Elab.Tactic.Tactic
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.Conv.evalNestedConv:
Lean.Elab.Tactic.Tactic
Equations
source
def Lean.Elab.Tactic.Conv.evalConvSeq:
Lean.Elab.Tactic.Tactic
Equations
source
def Lean.Elab.Tactic.Conv.evalConvConvSeq:
Lean.Elab.Tactic.Tactic
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.Conv.evalParen:
Lean.Elab.Tactic.Tactic
Equations
source
def Lean.Elab.Tactic.Conv.remarkAsConvGoal:
Lean.Elab.Tactic.TacticM Unit

Mark goals of the form ⊢ a = ?m .. with the conv goal annotation

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.Conv.evalNestedTacticCore:
Lean.Elab.Tactic.Tactic
Equations
source
def Lean.Elab.Tactic.Conv.evalNestedTactic:
Lean.Elab.Tactic.Tactic
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.Conv.evalConv:
Lean.Elab.Tactic.Tactic
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.Conv.evalFirst:
Lean.Elab.Tactic.Tactic
Equations