← Copula mathematical handbook

def Lean.Meta.Sym.isClass? (env : Environment) (type : Expr) : Option Name

Efficient version of Meta.isClass? for symbolic simulation. It does not use reduction nor instantiates metavariables.

Equations

• Lean.Meta.Sym.isClass? env type = Lean.Meta.Sym.isClass?.go✝ env type