package coq-stdpp-bitvector
- Overview
- No Docs
You can search for identifiers within the package.
in-package search v0.2.0
A library for bitvectors based on std++
Install
Dune Dependency
Authors
Maintainers
Sources
coq-stdpp-1.10.0.tar.gz
sha512=a20e2ef08d733bd2092c36d8956cfe7d431ee31cd7e74a8f9aafc5e4205bc04a778bbcb1ad35e62431789a3240280efbb8064aafd1eaa6a7a367fef55da6decd
Description
This library provides the bv n type for representing n-bit bitvectors (i.e.,
fixed-size integers with n bits). It comes with definitions for the standard operations
(e.g., the operations exposed by SMT-LIB) and some basic automation for solving bitvector
goals based on the lia tactic.
On This Page