Documentation

Mathlib.Util.AtomM

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.

Instances For

    The mutable state of the AtomM monad.

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

    Instances For
      @[reducible, inline]

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

      Equations
      Instances For
        def Mathlib.Tactic.AtomM.run {α : Type} (red : Lean.Meta.TransparencyMode) (m : Mathlib.Tactic.AtomM α) (evalAtom : optParam (Lean.ExprLean.MetaM Lean.Meta.Simp.Result) fun (e : Lean.Expr) => pure { expr := e, proof? := none, cache := true }) :

        Run a computation in the AtomM monad.

        Equations
        Instances For

          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.
          Instances For