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 (7)

Authors

Maintainers

M

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

Sources

formalv-1.4.0.tar.gz

sha512=10e582991ec1ba10f0d448500d6a87a6116a713ee74435ab80f8a61df5f0e4caa1f7d5e5239635e01c6204b3b75a6c2b3b9ae3c3f8925e0c7cf3f83e9dcfb506

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: 29 Oct 2025

Dependencies (3)

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

Dev Dependencies

None

Used by (2)

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

Conflicts