commit: 6a17e6252335f2594f693469fd29fde50c39da25

[log]
author: Luisa Cicolini <48860705+luisacicolini@users.noreply.github.com>

Mon Feb 17 03:02:37 2025 +0000
committer: GitHub <noreply@github.com>

Mon Feb 17 03:02:37 2025 +0000
tree: 46b2eb22251c47812d4e1fb6193013c6b638f9d4
parent: 1ce7047bf59931003defe8708006df490ee37486 [diff]

feat: add `BitVec.[(getMsbD, msb)_extractLsb', (getLsbD, getMsbD, msb)_extractLsb] `, add `and_eq_decide, or_eq_decide, decide_eq_true_iff` to `bool_to_prop ` (#6792)

This PR adds theorems `BitVec.(getMsbD, msb)_(extractLsb', extractLsb),
getMsbD_extractLsb'_eq_getLsbD`.

---------

Co-authored-by: Siddharth <siddu.druid@gmail.com>
Co-authored-by: Alex Keizer <alex@keizer.dev>
Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: Tobias Grosser <tobias@grosser.es>
Co-authored-by: Tobias Grosser <github@grosser.es>

3 files changed

tree: 46b2eb22251c47812d4e1fb6193013c6b638f9d4

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