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

Equations

• anchorRef.matches anchor = (anchorRef.anchorPrefix == anchor >>> (64 - anchorRef.numDigits.toUInt64 * 4))

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).

Equations

• Lean.Meta.Grind.getNumDigitsForAnchors es = Lean.Meta.Grind.getNumDigitsForAnchors.go✝ es 4

structure Lean.Meta.Grind.ExprWithAnchor : Type

• e : Expr
• anchor : UInt64

@[implicit_reducible]

instance Lean.Meta.Grind.instHasAnchorExprWithAnchor : HasAnchor ExprWithAnchor

Equations

• Lean.Meta.Grind.instHasAnchorExprWithAnchor = { getAnchor := fun (e : Lean.Meta.Grind.ExprWithAnchor) => e.anchor }

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Meta.Grind.mkAnchorSyntax numDigits anchor = Lean.Meta.Grind.mkAnchorSyntaxFromPrefix numDigits (anchor >>> (64 - 4 * numDigits.toUInt64))

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

Equations

• s.getAnchor = Lean.Meta.Grind.getAnchor s.getExpr