A monad for tracking and deduplicating atoms #
This monad is used by tactics like ring
and abel
to keep uninterpreted atoms in a consistent
order, and also to allow unifying atoms up to a specified transparency mode.
Note: this can become very expensive because it is using isDefEq
.
For performance reasons, consider whether Lean.Meta.Canonicalizer.canon
can be used instead.
After canonicalizing, a HashMap Expr Nat
suffices to keep track of previously seen atoms,
and is much faster as it uses Expr
equality rather than isDefEq
.
The context (read-only state) of the AtomM
monad.
The reducibility setting for definitional equality of atoms
- evalAtom : Lean.Expr → Lean.MetaM Lean.Meta.Simp.Result
A simplification to apply to atomic expressions when they are encountered, before interning them in the atom list.
Equations
- Mathlib.Tactic.AtomM.instInhabitedContext = { default := { red := default, evalAtom := default } }
The monad that ring
works in. This is only used for collecting atoms.
Run a computation in the AtomM
monad.
Equations
- Mathlib.Tactic.AtomM.run red m evalAtom = (m { red := red, evalAtom := evalAtom }).run' { atoms := #[] }
Get the index corresponding to an atomic expression, if it has already been encountered, or put it in the list of atoms and return the new index, otherwise.
Equations
- One or more equations did not get rendered due to their size.