package coq-hol-light-real

  1. Overview
  2. No Docs
Definition of HOL-Light real numbers in Coq

Install

Dune Dependency

github.com Edit opam file Versions (1)

Authors

  1. F
    Frédéric Blanqui

Maintainers

  1. 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, automatically generated from HOL-Light using hol2dk and lambdapi.

Tags

keyword:HOL-Light category:Math/Arith/Misc category:Math/Arith/Real numbers date:2024-11-03 logpath:HOLLight_Real

Published: 03 Nov 2024

Dependencies (1)

  1. coq >= "8.19"

Dev Dependencies

None

Used by (1)

  1. coq-hol-light >= "2.0.0"

Conflicts

None