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

Authors

Maintainers

M

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

Sources

formalv-1.3.0.tar.gz

sha256=a1045f3555371940e807046781e43702802560ef309c4be6cfe65088a8bf8347

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: 04 Feb 2025

Dependencies (3)

coq-mathcomp-ssreflect >= "2.3" & < "2.4~"
coq-mathcomp-algebra >= "2.3" & < "2.4~"
coq >= "8.19" & < "8.20~"

Dev Dependencies

None

Used by (2)

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

Conflicts