partial def Lean.Meta.performMatch (l : Array (Expr × Expr)) (protected_mvars : Array MVarId) : MetaM Bool

Given an array of expression pairs (match_target, e), attempts to assign mvars in e to make e equal to match_target (without making any assignments to mvars that appear in protected_mvars). Returns true and performs mvar assignments if successful, returns false and does not perform any mvar assignments otherwise

partial def Lean.Meta.performMatch.match1 (protected_mvars : Array MVarId) (match_target e : Expr) : Array MVarId → MetaM Bool

partial def Lean.Meta.performMatch.matchArgs (protected_mvars : Array MVarId) (match_target_tl e_tl : Array Expr) : MetaM Bool

partial def Lean.Meta.performMatch.matchRigidFlex (protected_mvars : Array MVarId) (match_target e : Expr) : Array MVarId → MetaM Bool

def Lean.Meta.performMatch.matchFlexFlex (match_target e : Expr) (protected_mvars : Array MVarId) : MetaM Bool

Equations

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