Helper functions for using the simplifier. #
[TODO] Needs documentation, cleanup, and possibly reunification of
mkSimpContext' with core.
ctx == false, the config argument is assumed to have type
ctx == false, the
discharge option must be none
mkSimpTheoremsFromConst except that it also returns the names of the generated
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.
mkSimpAttr except that it doesn't require syntax,
and returns an array of all auto-generated lemmas.
Simp.Context from a list of names.
Simplify an expression using only a list of lemmas specified by name.
Given a simplifier
S : Expr → MetaM Simp.Result,
and an expression
e : Expr, run
S on the type of
e, and then
e into that simplified type, using a combination of type hints and
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.