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.1.0.tar.gz
sha256=b571d859f20038aa10c51d863e8a0cce92646fc926ef706aa3d2d801a92ddac5

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.15" & < "1.16~"
  2. coq-mathcomp-algebra >= "1.15" & < "1.16~"
  3. coq >= "8.15" & < "8.17~"

Dev Dependencies

None

Used by (2)

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

Conflicts

None