Additional simp utilities #
This file adds additional tools for metaprogramming with the simp
tactic
@[inline]
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