Additional simp utilities

This file adds additional tools for metaprogramming with the simp tactic

@[inline]

def Lean.Meta.Simp.Methods.dischargeQ? (M : Methods) (a : Q(Prop)) : SimpM (Option Q(«$a»))

Qq version of Lean.Meta.Simp.Methods.discharge?, which avoids having to use ~q matching on the proof expression returned by discharge?

dischargeQ? (a : Q(Prop)) attempts to prove a using the discharger, returning some (pf : Q(a)) if a proof is found and none otherwise.

Equations

• M.dischargeQ? a = M.discharge? a