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

Preprocesses types that used for pattern matching and unification.

Equations

• Lean.Meta.Sym.preprocessType type = do let type ← Lean.Meta.Sym.unfoldReducible type let type ← liftM (Lean.Core.betaReduce type) Lean.Meta.zetaReduce type

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.