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

Authors

Maintainers

M

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

Sources

formalv-1.5.0.tar.gz

sha512=2524a34502ac80cce0c51e7a7426ab48e445a35c305699a5d9e1b0d7b69ea04d91cc94acd8dad944b363f1bd58f57299009b386c74b8ef5fec883cf98e5d1a3c

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: 04 Mar 2026

Dependencies (6)

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~")

Dev Dependencies

None

Used by (2)

Conflicts