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

1.0.0.tar.gz
sha256=69022c902c25d11245bc449059bb09203b3463dcbafe11944388a7b8f7631695

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: 25 Feb 2024

Dependencies (1)

  1. coq >= "8.19"

Dev Dependencies

None

Used by

None

Conflicts

None