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 (1)

Authors

Maintainers

M

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

Sources

formalv-1.5.0.tar.gz

sha512=2524a34502ac80cce0c51e7a7426ab48e445a35c305699a5d9e1b0d7b69ea04d91cc94acd8dad944b363f1bd58f57299009b386c74b8ef5fec883cf98e5d1a3c

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: 04 Mar 2026

Dependencies (7)

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~")

Dev Dependencies

None

Used by (1)

rocq-formalv-time

Conflicts