Additional utilities for Lean.Environment

def Lean.Environment.findConstValWithKind? (env : Environment) (decl : Name) (skipRealize : Bool := false) : Option (ConstantVal × ConstantKind)

Like findConstVal?, but also returns the declarations ConstantKind, which is known immediately.

Blocks on everything but the constant's body (if any), which is not accessible through the result.

def Lean.Environment.findConstValOfKind? (env : Environment) (p : ConstantKind → Bool) (decl : Name) (skipRealize : Bool := false) : Option ConstantVal

Like findConstVal?, but only finds the ConstantVal for decl in env if its kind satisfies p. Otherwise, returns none.

Blocks on everything but the constant's body (if any), which is not accessible through the result.

def Lean.Environment.findTheoremConstVal? (env : Environment) (decl : Name) (skipRealize : Bool := false) : Option ConstantVal

Like findConstVal?, but only finds the ConstantVal for decl in env if it is a theorem.

Blocks on everything but the constant's body (if any), which is not accessible through the result.