Documentation

Lean.Elab.Tactic.Conv.Simp

def Lean.Elab.Tactic.Conv.applySimpResult (result : Lean.Meta.Simp.Result) :

Lean.Elab.Tactic.TacticM Unit

Equations

Lean.Elab.Tactic.Conv.applySimpResult result = if Option.isNone result.proof? = true then Lean.Elab.Tactic.Conv.changeLhs result.expr else do let a ← liftM (Lean.Meta.Simp.Result.getProof result) Lean.Elab.Tactic.Conv.updateLhs result.expr a

def Lean.Elab.Tactic.Conv.evalSimp :

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.Conv.evalSimp stx = Lean.Elab.Tactic.withMainContext do let discr ← Lean.Elab.Tactic.mkSimpContext stx false false false let x : Lean.Elab.Tactic.MkSimpContextResult := discr match x with | { ctx := ctx, dischargeWrapper := dischargeWrapper, fvarIdToLemmaId := x } => do let lhs ← Lean.Elab.Tactic.Conv.getLhs let result ← Lean.Elab.Tactic.Simp.DischargeWrapper.with dischargeWrapper fun d? => liftM (Lean.Meta.simp lhs ctx d?) Lean.Elab.Tactic.Conv.applySimpResult result

def Lean.Elab.Tactic.Conv.evalSimpMatch :

Lean.Elab.Tactic.Tactic

Equations

Lean.Elab.Tactic.Conv.evalSimpMatch stx = Lean.Elab.Tactic.withMainContext do let a ← Lean.Elab.Tactic.Conv.getLhs let a ← liftM (Lean.Meta.Split.simpMatch a) Lean.Elab.Tactic.Conv.applySimpResult a