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.

ink

structure Mathlib.Tactic.AtomM.Context : Type

• The reducibility setting for definitional equality of atoms

  red : Lean.Meta.TransparencyMode

• 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.

ink

instance Mathlib.Tactic.AtomM.instInhabitedContext : Inhabited Mathlib.Tactic.AtomM.Context

Equations

• Mathlib.Tactic.AtomM.instInhabitedContext = { default := { red := default, evalAtom := default } }

ink

structure Mathlib.Tactic.AtomM.State : Type

• The list of atoms-up-to-defeq encountered thus far, used for atom sorting.

  atoms : Array Lean.Expr

The mutable state of the AtomM monad.

ink

@[inline]

abbrev Mathlib.Tactic.AtomM (α : Type) : Type

The monad that ring works in. This is only used for collecting atoms.

Equations

• Mathlib.Tactic.AtomM = ReaderT Mathlib.Tactic.AtomM.Context (StateRefT' IO.RealWorld Mathlib.Tactic.AtomM.State Lean.MetaM)

ink

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 }) : Lean.MetaM α

Run a computation in the AtomM monad.

Equations

• Mathlib.Tactic.AtomM.run red m evalAtom = StateRefT'.run' (m { red := red, evalAtom := evalAtom }) { atoms := #[] }

ink

def Mathlib.Tactic.AtomM.addAtom (e : Lean.Expr) : Mathlib.Tactic.AtomM ℕ

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.