@[reducible, inline]

abbrev Lean.Meta.UnificationHintKey : Type

structure Lean.Meta.UnificationHintEntry : Type

• keys : Array UnificationHintKey
• val : Name

@[implicit_reducible]

instance Lean.Meta.instInhabitedUnificationHintEntry : Inhabited UnificationHintEntry

def Lean.Meta.instInhabitedUnificationHintEntry.default : UnificationHintEntry

@[reducible, inline]

abbrev Lean.Meta.UnificationHintTree : Type

structure Lean.Meta.UnificationHints : Type

• discrTree : UnificationHintTree

@[implicit_reducible]

instance Lean.Meta.instInhabitedUnificationHints : Inhabited UnificationHints

def Lean.Meta.instInhabitedUnificationHints.default : UnificationHints

@[implicit_reducible]

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