Google Git Google Git
Sign in
fuchsia/third_party/github.com/leanprover/lean4/refs/heads/upstream/implicit_reducible_2
commit
c272f1a667fc842a95848db3a74ec0afc72719c3
[log]
author
Leonardo de Moura <leomoura@amazon.com>
Wed Feb 18 17:49:27 2026 -0800
committer
Kim Morrison <kim@tqft.net>
Thu Feb 19 22:37:08 2026 +0000
tree
5d93c224dab27fee7afc28e0b354194f2adbf49c
parent
3711f135dba19315542d23ba4d8ad407c5e49afa [diff] 
chore: remove unnecessary `set_option backward.isDefEq.respectTransparency false`

This PR removes 28 occurrences of `set_option backward.isDefEq.respectTransparency false in`
across 17 files that are no longer needed thanks to `[implicit_reducible]` annotations and
the `implicitBump` default.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
17 files changed
tree: 5d93c224dab27fee7afc28e0b354194f2adbf49c
  1. .claude/
  2. .github/
  3. doc/
  4. images/
  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 Install Lean.

Contributing

Please read our Contribution Guidelines first.

Building from Source

See Building Lean.