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

0.0.0.tar.gz
sha256=7e89265a208d33b1190487fc4a0d436d23df591c7ea7a2886a34a84460a5d4fa

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 date:2023-11-06 logpath:HOLLight

Published: 06 Nov 2023

Dependencies (1)

  1. coq >= "8.16"

Dev Dependencies

None

Used by

None

Conflicts

None