Helper functions for using the simplifier. #
[TODO] Needs documentation, cleanup, and possibly reunification of mkSimpContext'
with core.
Instances For
Instances For
Instances For
Instances For
Constructs a proof that the original expression is true
given a simp result which simplifies the target to True
.
Instances For
Return all propositions in the local context.
Instances For
If ctx == false
, the config argument is assumed to have type Meta.Simp.Config
,
and Meta.Simp.ConfigCtx
otherwise.
If ctx == false
, the discharge
option must be none
Instances For
Similar to mkSimpTheoremsFromConst
except that it also returns the names of the generated
lemmas.
Remark: either the length of the arrays is the same,
or the length of the first one is 0 and the length of the second one is 1.
Instances For
Similar to addSimpTheorem
except that it returns an array of all auto-generated
simp-theorems.
Instances For
Similar to AttributeImpl.add
in mkSimpAttr
except that it doesn't require syntax,
and returns an array of all auto-generated lemmas.
Instances For
Similar to AttributeImpl.add
in mkSimpAttr
except that it returns an array of all
auto-generated lemmas.
Instances For
Construct a Simp.Context
from a list of names.
Instances For
Simplify an expression using only a list of lemmas specified by name.
Instances For
Given a simplifier S : Expr → MetaM Simp.Result
,
and an expression e : Expr
, run S
on the type of e
, and then
convert e
into that simplified type, using a combination of type hints and Eq.mp
.
Instances For
Independently simplify both the left-hand side and the right-hand side of an equality. The equality is allowed to be under binders. Returns the simplified equality and a proof of it.
Instances For
Checks whether declName
is in SimpTheorems
as either a lemma or definition to unfold.
Instances For
Tests whether decl
has simp
-attribute simpAttr
. Returns false
is simpAttr
is not a
valid simp-attribute.
Instances For
Returns all declarations with the simp
-attribute simpAttr
.
Note: this also returns many auxiliary declarations.
Instances For
Gets all simp-attributes given to declaration decl
.