Lean 4 fork for HoTT-compatible kernel extensions (Path types, transport, HITs). Maintained against upstream leanprover/lean4.
372f344155
This PR resolves the following issues related to goal state display: 1. In a new line after a `case` tactic with a completed proof, the state of the proof in the `case` would be displayed, not the proof state after the `case` 1. In the range of `next =>` / `case' ... =>`, the state of the proof in the corresponding case would not be displayed, whereas this is true for `case` 1. In the `suffices ... by` tactic, the tactic state of the `by` block was not displayed after the `by` and before the first tactic The incorrect goal state after `case` was caused by `evalCase` adding a `TacticInfo` with the full block proof state for the full range of the `case` block that the goal state selection has no means of distinguishing from the `TacticInfo` with the same range that contains the state after the whole `case` block. Narrowing the range of this `TacticInfo` to `case ... =>` fixed this issue. The lack of a case proof state on `next =>` was caused by the `case` syntax that `next` expands to receiving noncanonical synthetic `SourceInfo`, which is usually ignored by the language server. Adding a token antiquotation for `next` fixed this issue. The lack of a case proof state on `case' ... =>` was caused by `evalCase'` not adding a `TacticInfo` with the full block state to the range of `case' ... =>`. Adding this `TacticInfo` fixed this issue. The tactic state of the block not being displayed after the `by` was caused by the macro expansion of `suffices` to `have` not transferring the trailing whitespace of the `by`. Ensuring that this trailing whitespace information is transferred fixed this issue. Fixes #2881. |
||
|---|---|---|
| .github | ||
| doc | ||
| images | ||
| nix | ||
| releases_drafts | ||
| script | ||
| src | ||
| stage0 | ||
| tests | ||
| .gitattributes | ||
| .gitignore | ||
| .ignore | ||
| CMakeLists.txt | ||
| CMakePresets.json | ||
| CODEOWNERS | ||
| CONTRIBUTING.md | ||
| debug.log | ||
| flake.lock | ||
| flake.nix | ||
| lean-toolchain | ||
| lean.code-workspace | ||
| LICENSE | ||
| LICENSES | ||
| README.md | ||
| RELEASES.md | ||
This is the repository for Lean 4.
About
- Quickstart
- Homepage
- Theorem Proving Tutorial
- Functional Programming in Lean
- Manual
- Release notes starting at v4.0.0-m3
- Examples
- External Contribution Guidelines
- FAQ
Installation
See Setting Up Lean.
Contributing
Please read our Contribution Guidelines first.
Building from Source
See Building Lean (documentation source: doc/make/index.md).