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 => x.fst) (Lean.PersistentHashMap.toList s.set)
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Meta.Simp.mkCast r e = do let __do_lift ← Lean.Meta.Simp.Result.getProof r Lean.Meta.mkAppM `cast #[__do_lift, e]
Return all propositions in the local context.
Equations
- One or more equations did not get rendered due to their size.
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
Equations
- One or more equations did not get rendered due to their size.
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.
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.
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.
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.
Construct a SimpTheorems
from a list of names. (i.e. as with simp only
).
Equations
- One or more equations did not get rendered due to their size.
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.
Given a simplifier S : Expr → MetaM Simp.Result→ 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.
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) || Lean.Meta.SimpTheorems.isDeclToUnfold d declName)
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.
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.
Gets all simp-attributes given to declaration decl
.
Equations
- One or more equations did not get rendered due to their size.