Documentation

Mathlib.Util.Simp

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
Instances For