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).

Wrap an 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.

Instances For