- decl: Lake.Name → Lean.Meta.Origin
A global declaration in the environment.
- fvar: Lean.FVarId → Lean.Meta.Origin
A local hypothesis. When
contextual := true
is enabled, this fvar may exist in an extension of the current local context; it will not be used for rewriting by simp once it is out of scope but it may end up in theusedSimps
trace. - stx: Lake.Name → Lean.Syntax → Lean.Meta.Origin
A proof term provided directly to a call to
simp [ref, ...]
whereref
is the provided simp argument (of kindParser.Tactic.simpLemma
). Theid
is a unique identifier for the call. - other: Lake.Name → Lean.Meta.Origin
Some other origin.
name
should not collide with the other types for erasure to work correctly, and simp trace will ignore this lemma. The other origins should be preferred if possible.
An Origin
is an identifier for simp theorems which indicates roughly
what action the user took which lead to this theorem existing in the simp set.
Instances For
A unique identifier corresponding to the origin.
Instances For
- keys : Array Lean.Meta.SimpTheoremKey
It stores universe parameter names for universe polymorphic proofs. Recall that it is non-empty only when we elaborate an expression provided by the user. When
proof
is just a constant, we can use the universe parameter names stored in the declaration.- proof : Lean.Expr
- priority : Nat
- post : Bool
- perm : Bool
perm
is true if lhs and rhs are identical modulo permutation of variables. - origin : Lean.Meta.Origin
origin
is mainly relevant for producing trace messages. It is also viewed anid
used to "erase"simp
theorems fromSimpTheorems
. - rfl : Bool
The fields levelParams
and proof
are used to encode the proof of the simp theorem.
If the proof
is a global declaration c
, we store Expr.const c []
at proof
without the universe levels, and levelParams
is set to #[]
When using the lemma, we create fresh universe metavariables.
Motivation: most simp theorems are global declarations, and this approach is faster and saves memory.
The field levelParams
is not empty only when we elaborate an expression provided by the user, and it contains universe metavariables.
Then, we use abstractMVars
to abstract the universe metavariables and create new fresh universe parameters that are stored at the field levelParams
.
Instances For
Instances For
Instances For
- post : Lean.Meta.SimpTheoremTree
- lemmaNames : Lean.PHashSet Lean.Meta.Origin
- toUnfold : Lean.PHashSet Lake.Name
- erased : Lean.PHashSet Lean.Meta.Origin
- toUnfoldThms : Lean.PHashMap Lake.Name (Array Lake.Name)
Instances For
Instances For
Instances For
Instances For
Return true
if declName
is tagged to be unfolded using unfoldDefinition?
(i.e., without using equational theorems).
Instances For
Instances For
Register the equational theorems for the given definition.
Instances For
Instances For
- thm: Lean.Meta.SimpTheorem → Lean.Meta.SimpEntry
- toUnfold: Lake.Name → Lean.Meta.SimpEntry
- toUnfoldThms: Lake.Name → Array Lake.Name → Lean.Meta.SimpEntry
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Auxiliary method for adding a global declaration to a SimpTheorems
datastructure.
Instances For
Instances For
Auxiliary method for adding a local simp theorem to a SimpTheorems
datastructure.