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.

structure Mathlib.Tactic.AtomM.Context : Type

• red : Lean.Meta.TransparencyMode

  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.

The context (read-only state) of the AtomM monad.

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

Equations

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

structure Mathlib.Tactic.AtomM.State : Type

• atoms : Array Lean.Expr

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

The mutable state of the AtomM monad.

@[inline, reducible]

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)

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 := #[] }

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

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.