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

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.

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.

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.