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

structure Lean.Meta.Grind.ExprWithAnchor : Type

• e : Expr
• anchor : UInt64

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