package rocq-formalv-check_range

Overview
Doc

You can search for identifiers within the package.

in-package search v0.2.0

Tactics to automatically prove Boolean goals involving Uint63/Sint63 variables

Install

Dune Dependency

gitlab.com Edit opam file Versions (2)

Authors

Maintainers

M

Mireia González Bedmar <mireia.gonzalez@formalv.com>

Sources

formalv-1.6.0.tar.gz

sha512=6126fcf580c61c718cb17f585f6c4a1c8171894c4c2809ec27a65e053d328994b7554081b4e7c79e4149c89f104e679f86ce37e6901de2c6fbddce57af546691

Description

FV Check Range provides tactics to automatically prove Boolean goals involving 1, 2 or 3 Uint63.int/Sint63.int bounded variables through brute-force computation.

Published: 20 Oct 2026

Dependencies (8)

rocq-formalv-prim63_mathcomp = version
rocq-mathcomp-algebra (>= "2.5.0" & < "2.6~")
rocq-mathcomp-order (>= "2.5.0" & < "2.6~")
rocq-mathcomp-boot (>= "2.5.0" & < "2.6~")
rocq-stdlib (>= "9.0" & < "9.1~")
coq-core (>= "9.0" & < "9.1~")
rocq-core (>= "9.0" & < "9.1~")
ocaml >= "4.10"

Dev Dependencies

None

Used by (1)

rocq-formalv-time >= "1.6.0"

Conflicts