@[inline, reducible]

abbrev Lean.Meta.UnificationHintKey : Type

structure Lean.Meta.UnificationHintEntry : Type

• keys : Array Lean.Meta.UnificationHintKey
• val : Lake.Name

instance Lean.Meta.instInhabitedUnificationHintEntry : Inhabited Lean.Meta.UnificationHintEntry

@[inline, reducible]

abbrev Lean.Meta.UnificationHintTree : Type

structure Lean.Meta.UnificationHints : Type

• discrTree : Lean.Meta.UnificationHintTree

instance Lean.Meta.instInhabitedUnificationHints : Inhabited Lean.Meta.UnificationHints

instance Lean.Meta.instToFormatUnificationHints : Lean.ToFormat Lean.Meta.UnificationHints

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

opaque Lean.Meta.unificationHintExtension : Lean.SimpleScopedEnvExtension Lean.Meta.UnificationHintEntry Lean.Meta.UnificationHints

structure Lean.Meta.UnificationConstraint : Type

• lhs : Lean.Expr
• rhs : Lean.Expr

structure Lean.Meta.UnificationHint : Type

• pattern : Lean.Meta.UnificationConstraint
• constraints : List Lean.Meta.UnificationConstraint

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

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

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

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