package coq-hol-light-real-with-nat

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 nat

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=40cb848c6f78e75e123d3e5383b1257705509f1c3aad00b620eca889eb826254

Description

This library provides a representation in Coq of the definition of real numbers in HOL-Light using the Coq type nat 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 = "2.0.0"

Conflicts