Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

feat: add DecidableRel instances for BitVec #24

Closed
wants to merge 1 commit into from
Closed

feat: add DecidableRel instances for BitVec #24

wants to merge 1 commit into from

Commits on Sep 27, 2024

  1. feat: add DecidableRel instances for BitVec 

    We follow the recipe for `Decidable` and create a decidable instance for
any bitvector width.

This was motivated in a case-bash that was used to prove an `sdiv` lemma at width 1.
However, due to file ordering constraints, we cannot we use the `DecidableRel`
machinery to implement the lemma `sdiv_eq_and`.
    @bollu
    bollu committed Sep 27, 2024
    Configuration menu
    Copy the full SHA
    8e1c843 View commit details
    Browse the repository at this point in the history