package coq-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 (7)

Authors

Maintainers

M

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

Sources

formalv-1.4.0.tar.gz

sha512=10e582991ec1ba10f0d448500d6a87a6116a713ee74435ab80f8a61df5f0e4caa1f7d5e5239635e01c6204b3b75a6c2b3b9ae3c3f8925e0c7cf3f83e9dcfb506

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: 29 Oct 2025

Dependencies (4)

coq-formalv-prim63_mathcomp = version
coq-mathcomp-algebra (>= "2.3.0" & < "2.4~")
coq-mathcomp-ssreflect (>= "2.3.0" & < "2.4~")
coq (>= "8.19" & < "8.21~")

Dev Dependencies

None

Used by (1)

coq-formalv-time >= "1.4.0"

Conflicts