Google Git Google Git
Sign in
fuchsia/third_party/github.com/leanprover/lean4/d1ec806834675f0c4f0614f52ff4b77e0035dc07
commit
d1ec806834675f0c4f0614f52ff4b77e0035dc07
[log]
author
jrr6 <7482866+jrr6@users.noreply.github.com>
Mon May 19 13:40:41 2025 -0400
committer
GitHub <noreply@github.com>
Mon May 19 17:40:41 2025 +0000
tree
8b974f6e5ab587eb581ab2ab28a48ac3af06c859
parent
b93231f97eacfa5fb33c7d736839abdd02b83bd9 [diff] 
feat: improve error messages in invalid match alternatives (#8368)

This PR improves the error messages produced by invalid pattern-match
alternatives and improves parity in error placement between
pattern-matching tactics and elaborators.

Closes #7170
35 files changed
tree: 8b974f6e5ab587eb581ab2ab28a48ac3af06c859
  1. .github/
  2. doc/
  3. images/
  4. nix/
  5. releases_drafts/
  6. script/
  7. src/
  8. stage0/
  9. tests/
  10. .gitattributes
  11. .gitignore
  12. .gitpod.Dockerfile
  13. .gitpod.yml
  14. .ignore
  15. CMakeLists.txt
  16. CMakePresets.json
  17. CODEOWNERS
  18. CONTRIBUTING.md
  19. flake.lock
  20. flake.nix
  21. lean-toolchain
  22. lean.code-workspace
  23. LICENSE
  24. LICENSES
  25. README.md
  26. RELEASES.md
README.md

This is the repository for Lean 4.

About

Installation

See Setting Up Lean.

Contributing

Please read our Contribution Guidelines first.

Building from Source

See Building Lean.