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.

Equations

• env.findConstValWithKind? decl skipRealize = do let info ← env.findAsync? decl skipRealize pure (info.toConstantVal, info.kind)

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.

Equations

• env.findConstValOfKind? p decl skipRealize = do let info ← env.findAsync? decl skipRealize if p info.kind = true then some info.toConstantVal else none

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.

Equations

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