package hol2dk
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=b9a304e56acda8367944c8590497ede7a386850b423432186309f36cc3aaed98
sha512=80027e2966d0b4192b5c297b6932ce10d7f20890be93e3f20570afb0ecd3b0b8f0ae84438a1f1aca5e8839e157240de8aedc772b3087c79b5c9ff2dca7792e7c
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.
1.0.0 (2024-02-25)
Added
add-links script
command rewrite to simplify prf files
command purge to compute useless theorems these two commands greatly reduce the size of generated proofs
command simp is equivalent to rewrite and purge
command dump-simp is equivalent to dump, pos, use and simp
allow simultaneous dumping
alignments of the types option, Sum, list, char, nadd
command split to generate a pos/use/sti/nbp file for each named theorem (an sti file contains the starting index of the corresponding proof)
command theorem to generate the lp files corresponding to a named theorem
Makefile to generate and check lp and coq files generated with split
command size to get statistics on the size of terms
option --print-stats to print statistics on hash tables at exit
use hash tables instead of maps to build abbreviations maps
use sharing when building canonical types and terms
add option --use-sharing for using sharing in lp output when defining term abbreviations
command nbp to get the number of proof steps
commands patch, unpatch and link to call the corresponding scripts
command env to print $HOL2DK_DIR and $HOLLIGHT_DIR
Modified
identifier renamings
merged the command dg in the command mk
fusion.ml: do not generate new theorems for empty instantiations
Fixed
valid dedukti and lambdapi identifiers
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.