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.2.0.tar.gz
sha256=7e01fa9f588e25d6b0ccaaeb4ba85439b3b7e16b9e16ab4c76be93d258e3de38

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: 24 Jul 2023

Dependencies (3)

  1. coq-mathcomp-ssreflect >= "1.13" & < "1.18~"
  2. coq-mathcomp-algebra >= "1.13" & < "1.18~"
  3. coq >= "8.14" & < "8.18~"

Dev Dependencies

None

Used by (2)

  1. coq-formalv-check_range >= "1.2.0"
  2. coq-formalv-time >= "1.2.0"

Conflicts

None