commit: bc6188a70a332ff85758c400517c720d552b90be

[log]
author: Siddharth <siddu.druid@gmail.com>

Sun Jun 23 23:37:02 2024 +0100
committer: GitHub <noreply@github.com>

Sun Jun 23 22:37:02 2024 +0000
tree: 04e0b0e4fb675697d226735e46522b0ac080301a
parent: 33f7865bbbccd8fbfffb1b4cb622d6f61dd42974 [diff]

feat: BitVec.twoPow and lemmas, toward bitblasting multiplication for LeanSAT (#4417)

We add a new definition `BitVec.twoPow w i` to represent `(1#w <<< i)`.
This expression is used to test bits when building the multiplication
bitblaster.

Patch 1/?, being peeled from https://github.com/opencompl/lean4/pull/6.

---------

Co-authored-by: Tobias Grosser <github@grosser.es>

3 files changed

tree: 04e0b0e4fb675697d226735e46522b0ac080301a

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).