partial def Lean.Meta.fastUnify (l : Array (Expr × Expr)) : MetaM Bool

partial def Lean.Meta.fastUnify.unify1 (s t : Expr) : MetaM Bool

partial def Lean.Meta.fastUnify.unifyArgs (ss tt : Array Expr) : MetaM Bool

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

Equations

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

partial def Lean.Meta.fastUnify.unifyFlexRigid (s t : Expr) : MetaM Bool