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

Equations

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

structure Lean.Meta.Grind.ExprWithAnchor : Type

• e : Expr
• anchor : UInt64

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