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

Authors

Maintainers

M

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

Sources

formalv-1.3.1.tar.gz

sha256=240a0294bfa990b4261662a86cf53bce44cd31672bbc69a9a3e667db5cc66ace

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: 13 May 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.20" & < "8.21~")

Dev Dependencies

None

Used by (1)

coq-formalv-time >= "1.3.1"

Conflicts