Documentation

Lean.Meta.UnificationHint

structure Lean.Meta.UnificationHintEntry:

Type

keys : Array Lean.Meta.DiscrTree.Key
val : Lean.Name

instance Lean.Meta.instInhabitedUnificationHintEntry:

Inhabited Lean.Meta.UnificationHintEntry

Equations

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

structure Lean.Meta.UnificationHints:

Type

discrTree : Lean.Meta.DiscrTree Lean.Name

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.format h.discrTree }

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 : Lean.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 : Lean.Name) :

Lean.MetaM Bool

Equations

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