Lean4
/-- If an atomic expression has already been encountered, get the index and the stored form of the
atom (which will be defeq at the specified transparency, but not necessarily syntactically equal).
If the atomic expression has *not* already been encountered, store it in the list of atoms, and
return the new index (and the stored form of the atom, which will be itself).
In a normalizing tactic, the expression returned by `addAtom` should be considered the normal form.
-/
def addAtom (e : Expr) : AtomM (Nat × Expr) := do
let c ← get
for h : i in [:c.atoms.size]do
if ← withTransparency (← read).red <| isDefEqSafe e c.atoms[i] then
return (i, c.atoms[i])
modifyGet fun c ↦ ((c.atoms.size, e), { c with atoms := c.atoms.push e })
