Anchor (aka stable hash) support for grind. We use anchors to reference terms in the grind state.

partial def Lean.Meta.Grind.getAnchor (e : Expr) : GrindM UInt64

def Lean.Meta.Grind.AnchorRef.matches (anchorRef : AnchorRef) (anchor : UInt64) : Bool

Example: { numDigits := 4, anchorPrefix := 0x0c88 }.matches 0x0c88ab10ef20206a returns true

class Lean.Meta.Grind.HasAnchor (α : Type u) : Type u

• getAnchor : α → UInt64

def Lean.Meta.Grind.getNumDigitsForAnchors {α : Type u_1} [HasAnchor α] (es : Array α) : Nat

Returns the number of digits needed to distinguish the anchors in es.

Elements with identical (full) anchors cannot be distinguished by adding more digits. Thus, they are ignored by this function. Callers must handle these collisions separately (e.g., the cases tactic uses ordinal references such as #a56e/2).

structure Lean.Meta.Grind.ExprWithAnchor : Type

• e : Expr
• anchor : UInt64

@[instance_reducible]

instance Lean.Meta.Grind.instHasAnchorExprWithAnchor : HasAnchor ExprWithAnchor

def Lean.Meta.Grind.mkAnchorSyntaxFromPrefix (numDigits : Nat) (anchorPrefix : UInt64) : CoreM (TSyntax `Lean.Parser.Tactic.anchor)

def Lean.Meta.Grind.mkAnchorSyntax (numDigits : Nat) (anchor : UInt64) : CoreM (TSyntax `Lean.Parser.Tactic.anchor)

def Lean.Meta.Grind.SplitInfo.getAnchor (s : SplitInfo) : GrindM UInt64