@[inline, reducible]

abbrev Lean.Meta.UnificationHintKey : Type

Equations

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

structure Lean.Meta.UnificationHintEntry : Type

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

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

Equations

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

@[inline, reducible]

abbrev Lean.Meta.UnificationHintTree : Type

Equations

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

structure Lean.Meta.UnificationHints : Type

• discrTree : Lean.Meta.UnificationHintTree

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

Equations

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

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

Equations

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

def Lean.Meta.UnificationHints.config : Lean.Meta.WhnfCoreConfig

Equations

• Lean.Meta.UnificationHints.config = { iota := false, beta := true, proj := Lean.Meta.ProjReductionKind.no, zeta := true }

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Lean.Meta.tryUnificationHints.isDefEqPattern p e = Lean.Meta.withReducible (Lean.Meta.isExprDefEqAux p e)

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

Equations

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