Helper functions for using the simplifier. #
[TODO] Needs documentation, cleanup, and possibly reunification of mkSimpContext'
with core.
Equations
- Lean.PHashSet.toList s = List.map (fun (x : α × Unit) => x.fst) (Lean.PersistentHashMap.toList s.set)
Instances For
Equations
- One or more equations did not get rendered due to their size.
Constructs a proof that the original expression is true
given a simp result which simplifies the target to True
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Return all propositions in the local context.
Equations
- One or more equations did not get rendered due to their size.
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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Similar to addSimpTheorem
except that it returns an array of all auto-generated
simp-theorems.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Similar to AttributeImpl.add
in mkSimpAttr
except that it doesn't require syntax,
and returns an array of all auto-generated lemmas.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Similar to AttributeImpl.add
in mkSimpAttr
except that it returns an array of all
auto-generated lemmas.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Construct a Simp.Context
from a list of names.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Simplify an expression using only a list of lemmas specified by name.
Equations
- One or more equations did not get rendered due to their size.
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
.
Equations
- One or more equations did not get rendered due to their size.
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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Checks whether declName
is in SimpTheorems
as either a lemma or definition to unfold.
Equations
- Lean.Meta.SimpTheorems.contains d declName = (Lean.Meta.SimpTheorems.isLemma d (Lean.Meta.Origin.decl declName true) || Lean.Meta.SimpTheorems.isDeclToUnfold d declName)
Instances For
Tests whether decl
has simp
-attribute simpAttr
. Returns false
is simpAttr
is not a
valid simp-attribute.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Returns all declarations with the simp
-attribute simpAttr
.
Note: this also returns many auxiliary declarations.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Gets all simp-attributes given to declaration decl
.
Equations
- One or more equations did not get rendered due to their size.