package coq-formalv-check_range

  1. Overview
  2. No Docs
Tactics to automatically prove Boolean goals involving Uint63/Sint63 variables

Install

Dune Dependency

gitlab.com Edit opam file Versions (4)

Authors

  1. A
    Ana de Almeida Borges
  2. Q
    Quim Casals Buñuel
  3. J
    Juan Conejero Rodriguez
  4. M
    Mireia González Bedmar
  5. E
    Eduardo Hermo Reyes

Maintainers

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

Sources

formalv-1.0.1.tar.gz
sha256=d00453d3f553c988df1ea1fd3a33413af03a2e21952b75b0c47f9290ae31b3bc

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.

Tags

keyword:automation keyword:primitive integers logpath:formalv

Published: 15 Nov 2022

Dependencies (4)

  1. coq-formalv-prim63_mathcomp = version
  2. coq-mathcomp-ssreflect >= "1.12" & < "1.15~"
  3. coq-mathcomp-algebra >= "1.12" & < "1.15~"
  4. coq >= "8.14" & < "8.16~"

Dev Dependencies

None

Used by (1)

  1. coq-formalv-time = "1.0.1"

Conflicts

None