def Lean.Meta.Sym.preprocessType (type : Expr) : MetaM Expr

Preprocesses types that used for pattern matching and unification.

def Lean.Meta.Sym.mkProofInstArgInfo? (xs : Array Expr) : MetaM (Option ProofInstInfo)

Analyzes whether the given free variables (aka arguments) are proofs or instances. Returns none if no arguments are proofs or instances.

def Lean.Meta.Sym.mkProofInstInfo? (declName : Name) : MetaM (Option ProofInstInfo)

Analyzes the type signature of declName and returns information about which arguments are proofs or instances. Returns none if no arguments are proofs or instances.

def Lean.Meta.Sym.getProofInstInfo? (declName : Name) : SymM (Option ProofInstInfo)

Returns information about the type signature of declName. It contains information about which arguments are proofs or instances. Returns none if no arguments are proofs or instances.