package coq-hol-light

  1. Overview
  2. No Docs
HOL-Light library in Coq

Install

Dune Dependency

github.com Edit opam file Versions (3)

Authors

  1. F
    Frédéric Blanqui

Maintainers

  1. F
    frederic.blanqui@inria.fr

Sources

2.0.0.tar.gz
sha256=83d65adc0147c53e2c013a6026593e38fdb0d47d84e098c8247d8553baefe8c0

Description

This library contains an automatic translation in Coq of (for the moment) some small part the HOL-Light library using https://github.com/Deducteam/hol2dk.

Tags

keyword:HOL-Light category:Math/Arith/Misc category:Math/Arith/Real Numbers category:Math/Real Numbers date:2024-12-17 logpath:HOLLight

Published: 17 Dec 2024

Dependencies (3)

  1. coq-fourcolor-reals >= "1.4.0"
  2. coq-hol-light-real >= "1.0"
  3. coq >= "8.19"

Dev Dependencies

None

Used by

None

Conflicts

None