Ecosyste.ms: Issues

An open API service for providing issue and pull request metadata for open source projects.

GitHub / Deducteam/hol2dk issues and pull requests

#50 - remove definitional axioms

Pull Request - State: closed - Opened by fblanqui over 1 year ago

#50 - remove definitional axioms

Pull Request - State: closed - Opened by fblanqui over 1 year ago

#49 - remove a few more axioms in coq

Pull Request - State: closed - Opened by fblanqui over 1 year ago

#49 - remove a few more axioms in coq

Pull Request - State: closed - Opened by fblanqui over 1 year ago

#48 - add nb_parts in dg file

Pull Request - State: closed - Opened by fblanqui over 1 year ago

#47 - improve hol2dk-exp and introduce environment variable HOL2DK_DIR

Pull Request - State: closed - Opened by fblanqui over 1 year ago

#46 - fix exp command

Pull Request - State: closed - Opened by fblanqui over 1 year ago

#45 - instrument BETA_CONV

Pull Request - State: closed - Opened by fblanqui over 1 year ago

#44 - instrument SYM

Pull Request - State: closed - Opened by fblanqui over 1 year ago

#43 - fix dg computation

Pull Request - State: closed - Opened by fblanqui over 1 year ago

#42 - add command to generate a file for each proof step (experimental)

Pull Request - State: closed - Opened by fblanqui over 1 year ago

#41 - reverse constants, axioms and definitions after reading

Pull Request - State: closed - Opened by fblanqui over 1 year ago

#40 - export ALPHA as REFL

Pull Request - State: closed - Opened by fblanqui over 1 year ago

#39 - change mk command

Pull Request - State: closed - Opened by fblanqui over 1 year ago

#38 - coq export: add more renamings

Pull Request - State: closed - Opened by fblanqui over 1 year ago

#37 - coq translation: remove more axioms

Pull Request - State: closed - Opened by fblanqui over 1 year ago

#36 - Translate HOL-Light types to non-empty types in Coq

Pull Request - State: closed - Opened by fblanqui over 1 year ago

#35 - fix following lambdapi update

Pull Request - State: closed - Opened by fblanqui almost 2 years ago

#34 - details

Pull Request - State: closed - Opened by fblanqui almost 2 years ago

#33 - fix v target and _CoqProject

Pull Request - State: closed - Opened by fblanqui almost 2 years ago

#32 - ci: check coq output

Pull Request - State: closed - Opened by fblanqui almost 2 years ago

#31 - add export to coq

Pull Request - State: closed - Opened by fblanqui almost 2 years ago

#30 - fix how to get theorem names (idx must be at the toplevel)

Pull Request - State: closed - Opened by fblanqui almost 2 years ago

#29 - instrument choose

Pull Request - State: closed - Opened by fblanqui almost 2 years ago

#28 - change type name translation

Pull Request - State: closed - Opened by fblanqui almost 2 years ago

#27 - optimize requires in lp files

Pull Request - State: closed - Opened by fblanqui almost 2 years ago

#26 - move some functions from main to xproof

Pull Request - State: closed - Opened by fblanqui almost 2 years ago

#25 - bug fixes

Pull Request - State: closed - Opened by fblanqui almost 2 years ago

#24 - lp: declare symbols as private whenever possible

Pull Request - State: closed - Opened by fblanqui almost 2 years ago

#23 - add ci for multi-threaded generation

Pull Request - State: closed - Opened by fblanqui almost 2 years ago

#22 - generate theorem names

Pull Request - State: closed - Opened by fblanqui almost 2 years ago

#21 - replace dump script by command

Pull Request - State: closed - Opened by fblanqui almost 2 years ago

#20 - cli: use first arg as command

Pull Request - State: closed - Opened by fblanqui almost 2 years ago

#19 - extend main with toplevel-independent commands of xnames

Pull Request - State: closed - Opened by fblanqui almost 2 years ago

#18 - Rename hol_theory.dk/lp into theory_hol.dk/lp

Pull Request - State: closed - Opened by fblanqui almost 2 years ago

#17 - create pos file to speed up proof file generation

Pull Request - State: closed - Opened by fblanqui almost 2 years ago

#16 - put nb_proofs first in sig file and minimize sig file reading

Pull Request - State: closed - Opened by fblanqui almost 2 years ago

#15 - fix variable naming

Pull Request - State: closed - Opened by fblanqui almost 2 years ago

#14 - add parallel dk file generation

Pull Request - State: closed - Opened by fblanqui almost 2 years ago

#13 - fix translation of names

Pull Request - State: closed - Opened by fblanqui almost 2 years ago

#12 - do not abbrev constants

Pull Request - State: closed - Opened by fblanqui almost 2 years ago

#11 - add parallel lp generation

Pull Request - State: closed - Opened by fblanqui almost 2 years ago

#10 - modify parsing of arguments

Pull Request - State: closed - Opened by fblanqui almost 2 years ago

#9 - make lp output more modular

Pull Request - State: closed - Opened by fblanqui almost 2 years ago

#8 - change dump filenames

Pull Request - State: closed - Opened by fblanqui almost 2 years ago

#7 - don't load proofs in memory + some bug fixes

Pull Request - State: closed - Opened by fblanqui almost 2 years ago

#6 - Move functions to access proofs in a separate module

Pull Request - State: closed - Opened by fblanqui almost 2 years ago

#5 - details

Pull Request - State: closed - Opened by fblanqui almost 2 years ago

#4 - add HOL-Light file to compute named theorems and file dependencies

Pull Request - State: closed - Opened by fblanqui almost 2 years ago

#3 - instrument intro/elim rules

Pull Request - State: closed - Opened by fblanqui almost 2 years ago

#2 - CI: use Deducteam repo for Lambdapi

Pull Request - State: closed - Opened by fblanqui almost 2 years ago

#1 - Add CI

Pull Request - State: closed - Opened by fblanqui almost 2 years ago