Lean 4 fork for HoTT-compatible kernel extensions (Path types, transport, HITs). Maintained against upstream leanprover/lean4.
7cdf917c97
Consider the following example ```lean def div!: Nat → Nat → Nat | x, 0 => panic! "division by zero" | x, y => x/y def weird (x : Nat) : MetaM Nat := unless (x > 0) (throwOther "x == 0") *> let y := div! 10 x; pure y ``` If we execute `weird 0`, it produces a "division by zero" panic message. This is a simple version of a much bigger function in the new frontend. This is not due to a bug in the compiler. It produces the panic message because of the `do`-encoding refactoring. Recall that, a few months ago, we started to compile `do a; b` as `a *> b` (i.e., `seqRight a b`). Thus, the example above is `seqRight action1 (let y := div! 10 x; pure y)` where `action1` is the `unless ...`. In A-normal form, this is equivalent to ```lean let y:= div! 10 x; let action2 := pure y; seqRight action1 action2 ``` Thus, we execute `div! 10 x` before we even execute the `seqRight`. This is counterintuitive and demonstrates once again how impure features such as `panic!` are dangerous. This commit reverts the `do`-encoding refactoring, and encodes `do a; b` as `a >>= fun _ b` as we did in Lean3. cc @Kha |
||
|---|---|---|
| .github | ||
| doc | ||
| images | ||
| lean4-mode | ||
| nix | ||
| script | ||
| src | ||
| stage0 | ||
| tests | ||
| tmp | ||
| .clang-format | ||
| .codecov.yml | ||
| .gitattributes | ||
| .gitignore | ||
| CMakeLists.txt | ||
| default.nix | ||
| LICENSE | ||
| README.md | ||
| shell.nix | ||
We are currently developing Lean 4. Lean 3 is still the latest official release. This repository contains work in progress.
Important. Unless you are one of our collaborators
- We strongly suggest you use Lean 3.
- Pull requests are not welcome.
- New issues are not welcome, and will be closed without any feedback.