package coq-formalv-prim63_mathcomp

Overview
Doc

You can search for identifiers within the package.

in-package search v0.2.0

Refinements from MathComp nat and int to Coq primitive integers Uint63/Sint63

Install

Dune Dependency

gitlab.com Edit opam file Versions (6)

Authors

Maintainers

M

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

Sources

formalv-1.3.1.tar.gz

sha256=240a0294bfa990b4261662a86cf53bce44cd31672bbc69a9a3e667db5cc66ace

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.

Published: 13 May 2025

Dependencies (3)

coq-mathcomp-algebra (>= "2.3.0" & < "2.4~")
coq-mathcomp-ssreflect (>= "2.3.0" & < "2.4~")
coq (>= "8.20" & < "8.21~")

Dev Dependencies

None

Used by (2)

coq-formalv-check_range >= "1.3.1"
coq-formalv-time >= "1.3.1"

Conflicts