package hol2dk

  1. Overview
  2. Docs
HOL-Light to Dedukti/Lambdapi translator

Install

Dune Dependency

Authors

Maintainers

Sources

hol2dk-0.0.1.tbz
sha256=e1d729676f01c0fdfcffaa06be212caa80316dcdccdea77fe3c0973c14fe641d
sha512=7be0c83ef0356ce18889f447a1183c4ec5373c2a47291ceb9c75d426fe159cd824db95b01285f8da805fbd002fdcb91cb59666e31535c3c84cac92075feefd63

CHANGES.md.html

CHANGES.md

All notable changes to this project will be documented in this file.

The format is based on Keep a Changelog, and this project adheres to Semantic Versioning.

0.0.1 (2023-11-22)

Added

  • add command dump-use for dumping a file without including "hol.ml"

Modified

  • rename mk-part command into mk

  • the dump command now includes "hol.ml"

  • do not print ocaml warnings while dumping proofs

  • do not export unused proofs (about 7%)

  • make hol2dk stat give the number of unused proofs

Fixed

  • README.md

  • output of hol2dk axm

  • output of hol2dk mk

0.0.0 (2023-11-08)

First release.