This module implements analysis tools for e-matching instantiation graphs. They are used to provide the user insights on potential issues with e-matching in a proof.

def Lean.Meta.Grind.mkEMatchDiagMessages (trace : PArray EMatchDiagInfo) (counters : Counters) : MetaM (Option MessageData)

Equations

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