commit: c0aca6a84e8619b258a6aefdf716407a85382a7c

[log]
author: Sebastian Ullrich <sebasti@nullri.ch>

Sat Nov 07 22:13:13 2026 +0000
committer: Sebastian Ullrich <sebasti@nullri.ch>

Sat Nov 07 22:13:15 2026 +0000
tree: 2cc757766a79bb113a63f638833018dcf1baa60c
parent: 1df56a5104b486c8121e57c0e78d20a6b851beb9 [diff]

WIP: keep `checked` semantics via a separate unchecked kernel environment chain

Kernel checks now run against the new `Environment.uncheckedKernelEnv`, which contains preceding declarations before their checks have finished, while `checked` still waits for each check result and replaces rejected declarations with axioms as before.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

3 files changed

tree: 2cc757766a79bb113a63f638833018dcf1baa60c

README.md

This is the repository for Lean 4.

About

Installation

See Install Lean.

Contributing

Please read our Contribution Guidelines first.

Building from Source

See Building Lean.