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

Preprocesses types that used for pattern matching and unification.

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

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