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.0.tar.gz
sha256=73143b71400fefb310144640cac71cf6abafdc06a6f6acc29d024a42b91eabdc

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: 08 Jul 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