Lean 4 fork for HoTT-compatible kernel extensions (Path types, transport, HITs). Maintained against upstream leanprover/lean4.
145bd50903
@Kha Patterns with nested "choice" nodes produce counterintuitive behavior, and hard to understand errors. They only work when we have the exact same overloads at macro definition and application time. Here is a funky example ``` syntax [myAdd] term "++":65 term:65 : term -- overloads "++" /- The following `macro_rules` manages to eliminate "choice" node by using the explicitly provided node kind. -/ macro_rules [myAdd] `($a ++ $b) => `($a + $b) check (1:Nat) ++ 2 -- works as expected syntax "FOO!" term : term /- Before this commit, the following pattern was accepted, and it contained a "choice" node for `++`. It is a `myAdd` or `HasAppend.append`. Now, this kind of pattern is rejected since it contains a nested "choice" -/ macro_rules `(FOO! $a ++ $b) => `($a ++ $b) /- Before this commit, the following command worked because it contained a "choice" node similar to the one at macro definition time. -/ check FOO! [1, 2] ++ [2, 3] -- Now, we have 3 overloads for "++". syntax [myAppend] term "++":65 term:65 : term -- The `macro_rules` fails here. ``` This commit fixes this weird behavior by disallowing "choice" nodes in patterns. |
||
|---|---|---|
| .github | ||
| bin | ||
| doc | ||
| images | ||
| lean4-mode | ||
| nix | ||
| script | ||
| src | ||
| stage0 | ||
| tests | ||
| tmp | ||
| .clang-format | ||
| .codecov.yml | ||
| .gitattributes | ||
| .gitignore | ||
| 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.