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

Authors

H

https://github.com/Deducteam/coq-hol-light-real-with-N/blob/main/AUTHORS.md

Maintainers

F

frederic.blanqui@inria.fr

Sources

2.0.0.tar.gz

sha256=2c9a3786a627e5a6e806c06c96e5b940e0b399c0d2253bfdeb3f83db44bf8d71

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: 11 Jul 2025

Dependencies (1)

rocq-prover >= "9.0"

Dev Dependencies

None

Used by (1)

coq-hol-light >= "3.0.0"

Conflicts