Lean.Kernel.Environment.replay

replay env constantMap will "replay" all the constants in constantMap : HashMap Name ConstantInfo into env, sending each declaration to the kernel for checking.

replay does not send constructors or recursors in constantMap to the kernel, but rather checks that they are identical to constructors or recursors generated in the environment after replaying any inductive definitions occurring in constantMap.

replay can be used either as:

• a verifier for a Kernel.Environment, by sending everything to the kernel, or
• a mechanism to safely transfer constants from one Kernel.Environment to another.

def Lean.Kernel.Environment.replay (newConstants : Std.HashMap Name ConstantInfo) (env : Environment) : IO Environment

"Replay" some constants into a Kernel.Environment, sending them to the kernel for checking.

Throws a IO.userError if the kernel rejects a constant, or if there are malformed recursors or constructors for inductive types.

Equations

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

@[deprecated Lean.Kernel.Environment.replay (since := "2026-07-14")]

def Lean.Environment.replay (newConstants : Std.HashMap Name ConstantInfo) (env : Environment) : IO Environment

Equations

• Lean.Environment.replay newConstants env = do let __do_lift ← Lean.Kernel.Environment.replay newConstants env.toKernelEnv pure (Lean.Environment.ofKernelEnv __do_lift)