chore: bv_decide remove noop rewrites

leanprover / lean4

Lean 4 programming language and theorem prover

https://lean-lang.org

Apache License 2.0

4.74k stars 427 forks source link

Closed hargoniX closed 1 week ago

hargoniX commented 1 week ago

Merely removes rules that are actually just syntactic aliases but equal at the Expr level.

leanprover-community-bot commented 1 week ago

Mathlib CI status (docs):

❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e0d7c3ac79bd9167ce7d295f51bf3779a04f7a07 --onto 1315266dd3faeaf28d1263668cb88f2f3f5e530c. (2024-11-14 19:28:45)