Lean.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 an
Environment
, by sending everything to the kernel, or - a mechanism to safely transfer constants from one
Environment
to another.
- newConstants : Std.HashMap Lean.Name Lean.ConstantInfo
Instances For
- env : Lean.Environment
- remaining : Lean.NameSet
- pending : Lean.NameSet
- postponedConstructors : Lean.NameSet
- postponedRecursors : Lean.NameSet
Instances For
Equations
Instances For
Use the current Environment
to throw a KernelException
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Add a declaration, possibly throwing a KernelException
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Check if a Name
still needs to be processed (i.e. is in remaining
).
If so, recursively replay any constants it refers to, to ensure we add declarations in the right order.
The construct the Declaration
from its stored ConstantInfo
,
and add it to the environment.
Replay a set of constants one at a time.
Check that all postponed constructors are identical to those generated when we replayed the inductives.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Check that all postponed recursors are identical to those generated when we replayed the inductives.
Equations
- One or more equations did not get rendered due to their size.
Instances For
"Replay" some constants into an 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.