package coq-bits

  1. Overview
  2. No Docs
A bit vector library

Install

Dune Dependency

github.com Edit opam file Versions (2)

Authors

  1. A
    Andrew Kennedy <akenn@microsoft.com>
  2. A
    Arthur Blot <arthur.blot@ens-lyon.fr>
  3. P
    Pierre-Évariste Dagand <pierre-evariste.dagand@lip6.fr>

Maintainers

  1. A
    anton.a.trunov@gmail.com

Sources

1.1.0.tar.gz
sha512=7e7ff1503c936977ce77e8d74e5aa9bec375e33d640d20baa3ea277dc5db3724aaa52aa16d09dbd9ccbdf2192bcc133d86bbfb0cca79164a8921e2643c27a855

Description

A formalization of bitset operations in Coq and the corresponding axiomatization and extraction to OCaml native integers

Tags

category:Computer Science/Data Types and Data Structures keyword:bit arithmetic keyword:bitset keyword:bit vector keyword:extraction logpath:Bits date:2021-07-11

Published: 12 Jul 2021

Dependencies (2)

  1. coq-mathcomp-algebra (>= "1.12" & < "1.16~")
  2. coq (>= "8.10" & < "8.17~")

Dev Dependencies

None

Used by

None

Conflicts

None