@[reducible, inline]

abbrev Lean.Meta.UnificationHintKey : Type

Equations

• Lean.Meta.UnificationHintKey = Lean.Meta.DiscrTree.Key

structure Lean.Meta.UnificationHintEntry : Type

• keys : Array UnificationHintKey
• val : Name

instance Lean.Meta.instInhabitedUnificationHintEntry : Inhabited UnificationHintEntry

Equations

• Lean.Meta.instInhabitedUnificationHintEntry = { default := Lean.Meta.instInhabitedUnificationHintEntry.default }

def Lean.Meta.instInhabitedUnificationHintEntry.default : UnificationHintEntry

Equations

• Lean.Meta.instInhabitedUnificationHintEntry.default = { keys := default, val := default }

@[reducible, inline]

abbrev Lean.Meta.UnificationHintTree : Type

Equations

• Lean.Meta.UnificationHintTree = Lean.Meta.DiscrTree Lean.Name

structure Lean.Meta.UnificationHints : Type

• discrTree : UnificationHintTree

instance Lean.Meta.instInhabitedUnificationHints : Inhabited UnificationHints

Equations

• Lean.Meta.instInhabitedUnificationHints = { default := Lean.Meta.instInhabitedUnificationHints.default }

def Lean.Meta.instInhabitedUnificationHints.default : UnificationHints

Equations

• Lean.Meta.instInhabitedUnificationHints.default = { discrTree := default }

instance Lean.Meta.instToFormatUnificationHints : ToFormat UnificationHints

Equations

• Lean.Meta.instToFormatUnificationHints = { format := fun (h : Lean.Meta.UnificationHints) => Std.format h.discrTree }

def Lean.Meta.UnificationHints.add (hints : UnificationHints) (e : UnificationHintEntry) : UnificationHints

Equations

• hints.add e = { discrTree := Lean.Meta.DiscrTree.insertCore hints.discrTree e.keys e.val }

opaque Lean.Meta.unificationHintExtension : SimpleScopedEnvExtension UnificationHintEntry UnificationHints

structure Lean.Meta.UnificationConstraint : Type

• lhs : Expr
• rhs : Expr

structure Lean.Meta.UnificationHint : Type

• pattern : UnificationConstraint
• constraints : List UnificationConstraint

def Lean.Meta.addUnificationHint (declName : Name) (kind : AttributeKind) : MetaM Unit

Equations

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

def Lean.Meta.tryUnificationHints (t s : Expr) : MetaM Bool

Equations

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