Dischargers for simp to tactics

This file defines a wrapper for Simp.Dischargers as regular tactics, that allows them to be used via the tactic frontend of simp via simp (discharger := wrapSimpDischarger my_discharger).

def wrapSimpDischarger (dis : Lean.Meta.Simp.Discharge) : Lean.Elab.Tactic.TacticM Unit

Wrap a simp discharger (a function Expr → SimpM (Option Expr)) as a tactic, so that it can be passed as an argument to simp (discharger := foo). This is inverse to mkDischargeWrapper.

Equations

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