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

Authors

F

Frédéric Blanqui

Maintainers

F

frederic.blanqui@inria.fr

Sources

1.1.0.tar.gz

sha256=16554b342f29484ea2bd9f4057c3a15e67af4ef49d9d56e06cae03d0406ec009

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

Dependencies (1)

coq >= "8.19"

Dev Dependencies

None

Used by (1)

coq-hol-light >= "3.0.0"

Conflicts