⚠️ Under construction ⚠️ This website will be officialy launched with the first release of Rocq 9.0 in March 2025. Until then, there may remain broken links and references to not-yet existing projects.

package coq-hol-light-real-with-N

Overview
Doc

You can search for identifiers within the package.

in-package search v0.2.0

Definition of HOL-Light real numbers in Coq using N

Install

Dune Dependency

github.com Edit opam file Versions (1)

Authors

F

Frédéric Blanqui

Maintainers

F

frederic.blanqui@inria.fr

Sources

1.0.0.tar.gz

sha256=b4e60de1322965dc6daf7beb63fd7ff270e341e162428fddd1ac5e32e47054b5

Description

This library provides a representation in Coq of the definition of real numbers in HOL-Light, using the Coq type N for natural numbers, automatically generated from HOL-Light using hol2dk and lambdapi.

Published: 20 Jan 2025

Dependencies (1)

coq >= "8.19"

Dev Dependencies

None

Used by (1)

coq-hol-light >= "3.0.0"

Conflicts