@[reducible, inline]

abbrev Lean.Meta.UnificationHintKey : Type

structure Lean.Meta.UnificationHintEntry : Type

• keys : Array UnificationHintKey
• val : Name

instance Lean.Meta.instInhabitedUnificationHintEntry : Inhabited UnificationHintEntry

@[reducible, inline]

abbrev Lean.Meta.UnificationHintTree : Type

structure Lean.Meta.UnificationHints : Type

• discrTree : UnificationHintTree

instance Lean.Meta.instInhabitedUnificationHints : Inhabited UnificationHints

instance Lean.Meta.instToFormatUnificationHints : ToFormat UnificationHints

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

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

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

def Lean.Meta.tryUnificationHints.isDefEqPattern (p e : Expr) : MetaM Bool

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