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.
The reducibility setting for definitional equality of atoms
A simplification to apply to atomic expressions when they are encountered, before interning them in the atom list.
evalAtom : Lean.Expr → Lean.MetaM Lean.Meta.Simp.Result
The context (read-only state) of the AtomM
monad.
Instances For
Equations
- Mathlib.Tactic.AtomM.instInhabitedContext = { default := { red := default, evalAtom := default } }
@[inline]
The monad that ring
works in. This is only used for collecting atoms.
def
Mathlib.Tactic.AtomM.run
{α : Type}
(red : Lean.Meta.TransparencyMode)
(m : Mathlib.Tactic.AtomM α)
(evalAtom : optParam (Lean.Expr → Lean.MetaM Lean.Meta.Simp.Result) fun e => pure { expr := e, proof? := none, dischargeDepth := 0 })
:
Run a computation in the AtomM
monad.
Equations
- Mathlib.Tactic.AtomM.run red m evalAtom = StateRefT'.run' (m { red := red, evalAtom := evalAtom }) { 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.