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

Authors

Maintainers

M

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

Sources

formalv-1.3.0.tar.gz

sha256=a1045f3555371940e807046781e43702802560ef309c4be6cfe65088a8bf8347

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 Feb 2025

Dependencies (4)

coq-formalv-prim63_mathcomp = version
coq-mathcomp-ssreflect >= "2.3" & < "2.4~"
coq-mathcomp-algebra >= "2.3" & < "2.4~"
coq >= "8.19" & < "8.20~"

Dev Dependencies

None

Used by (1)

coq-formalv-time >= "1.3.0"

Conflicts