package rocq-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 Rocq primitive integers Uint63/Sint63

Install

Dune Dependency

gitlab.com Edit opam file Versions (2)

Authors

Maintainers

M

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

Sources

formalv-1.6.0.tar.gz

sha512=6126fcf580c61c718cb17f585f6c4a1c8171894c4c2809ec27a65e053d328994b7554081b4e7c79e4149c89f104e679f86ce37e6901de2c6fbddce57af546691

Description

FV Prim63 to MathComp provides conversions from the Rocq 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: 20 Oct 2026

Dependencies (7)

rocq-mathcomp-algebra (>= "2.5.0" & < "2.6~")
rocq-mathcomp-order (>= "2.5.0" & < "2.6~")
rocq-mathcomp-boot (>= "2.5.0" & < "2.6~")
rocq-stdlib (>= "9.0" & < "9.1~")
coq-core (>= "9.0" & < "9.1~")
rocq-core (>= "9.0" & < "9.1~")
ocaml >= "4.10"

Dev Dependencies

None

Used by (2)

rocq-formalv-check_range >= "1.6.0"
rocq-formalv-time >= "1.6.0"

Conflicts