commit: fc5201584166e35fadb7d0fe2bd2b8b59450b155

[log]
author: Tobias Grosser <tobias@grosser.es>

Sun Sep 22 11:10:54 2024 +0100
committer: GitHub <noreply@github.com>

Sun Sep 22 10:10:54 2024 +0000
tree: 62db83ca6b84ad86972fcd77e2e2e3743147e9f8
parent: a6830f90ab365e14ccb7ca31201de37f8c1e978c [diff]

feat: add `_self`, `_zero`, and `_allOnes` for BitVec.[and|or|xor] (#5413)

The `xor_allOnes` theorems end up in the `not` section, as the relevant
simplification lemmas are otherwise not defined.

src/Init/Data/BitVec/Lemmas.lean[diff]

1 file changed

tree: 62db83ca6b84ad86972fcd77e2e2e3743147e9f8

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 (documentation source: doc/make/index.md).