package coq-formalv-prim63_mathcomp

  1. Overview
  2. No Docs
Refinements from MathComp nat and int to Coq primitive integers Uint63/Sint63

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 Prim63 to MathComp provides conversions from the Coq primitive integers Uint63 and Sint63 to the MathComp natural and integer numbers nat and int, and vice versa, as well as lemmas to rewrite between their respective operations.

Tags

keyword:refinement keyword:primitive integers logpath:formalv

Published: 15 Nov 2022

Dependencies (3)

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

Dev Dependencies

None

Used by (2)

  1. coq-formalv-check_range = "1.0.1"
  2. coq-formalv-time = "1.0.1"

Conflicts

None