Deducteam/hol2dk issues and pull requests

#135 - align real numbers properties

Pull Request - State: open - Opened by fblanqui 8 months ago

#100 - fix add-links

Pull Request - State: closed - Opened by fblanqui 11 months ago

#100 - fix add-links

Pull Request - State: closed - Opened by fblanqui 11 months ago

#99 - define term abbrevs over several files if needed

Pull Request - State: closed - Opened by fblanqui 11 months ago

#99 - define term abbrevs over several files if needed

Pull Request - State: closed - Opened by fblanqui 11 months ago

#98 - update README.md

Pull Request - State: closed - Opened by fblanqui 11 months ago

#98 - update README.md

Pull Request - State: closed - Opened by fblanqui 11 months ago

#97 - dune-project: add documentation stanza

Pull Request - State: closed - Opened by fblanqui 11 months ago

#97 - dune-project: add documentation stanza

Pull Request - State: closed - Opened by fblanqui 11 months ago

#96 - add mapping of char to ascii

Pull Request - State: closed - Opened by fblanqui 11 months ago

#96 - add mapping of char to ascii

Pull Request - State: closed - Opened by fblanqui 11 months ago

#95 - prepare release

Pull Request - State: closed - Opened by fblanqui 11 months ago

#95 - prepare release

Pull Request - State: closed - Opened by fblanqui 11 months ago

#94 - add opam target in Makefile + update TODO

Pull Request - State: closed - Opened by fblanqui 11 months ago

#94 - add opam target in Makefile + update TODO

Pull Request - State: closed - Opened by fblanqui 11 months ago

#93 - complete mapping up to `nadd`

Pull Request - State: closed - Opened by AnthonyBordg 12 months ago - 4 comments

#93 - complete mapping up to `nadd`

Pull Request - State: closed - Opened by AnthonyBordg 12 months ago - 4 comments

#92 - Improve Makefile

Pull Request - State: closed - Opened by fblanqui 12 months ago

#92 - Improve Makefile

Pull Request - State: closed - Opened by fblanqui 12 months ago

#91 - add commands for calling scripts

Pull Request - State: closed - Opened by fblanqui 12 months ago

#91 - add commands for calling scripts

Pull Request - State: closed - Opened by fblanqui 12 months ago

#90 - use valid coq filenames + add command nbp

Pull Request - State: closed - Opened by fblanqui 12 months ago

#90 - use valid coq filenames + add command nbp

Pull Request - State: closed - Opened by fblanqui 12 months ago

#89 - fix #86 + remove commands for one file by proof

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

#89 - fix #86 + remove commands for one file by proof

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

#88 - add sharing in the definitions of abbreviations

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

#88 - add sharing in the definitions of abbreviations

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

#87 - Variable names with underscores

Issue - State: closed - Opened by thomastraversie about 1 year ago

#87 - Variable names with underscores

Issue - State: closed - Opened by thomastraversie about 1 year ago

#86 - Multiple abbreviations

Issue - State: closed - Opened by thomastraversie about 1 year ago - 1 comment

#86 - Multiple abbreviations

Issue - State: closed - Opened by thomastraversie about 1 year ago - 1 comment

#85 - Bump actions/checkout from 3 to 4

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

#85 - Bump actions/checkout from 3 to 4

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

#84 - add renamings

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

#84 - add renamings

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

#83 - use maximal sharing for building abbreviation maps

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

#83 - use maximal sharing for building abbreviation maps

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

#82 - fix Makefile and add-links

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

#82 - fix Makefile and add-links

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

#81 - rename stp into sti + enable stat on split files

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

#81 - rename stp into sti + enable stat on split files

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

#80 - Create a pos/use file for each global theorem

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

#80 - Create a pos/use file for each global theorem

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

#79 - add mappings of `sum_type`, `list`, `char` and `nadd`

Pull Request - State: closed - Opened by AnthonyBordg about 1 year ago - 3 comments

#79 - add mappings of `sum_type`, `list`, `char` and `nadd`

Pull Request - State: closed - Opened by AnthonyBordg about 1 year ago - 3 comments

#78 - add mapping of 'sum_type'

Pull Request - State: closed - Opened by AnthonyBordg about 1 year ago

#78 - add mapping of 'sum_type'

Pull Request - State: closed - Opened by AnthonyBordg about 1 year ago

#77 - extend mapping to ZRECSPACE and the types recspace and option

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

#77 - extend mapping to ZRECSPACE and the types recspace and option

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

#76 - inline nb_proofs()

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

#76 - inline nb_proofs()

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

#75 - merge the command dg in the command mk

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

#75 - merge the command dg in the command mk

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

#74 - rewrite: use a map to proof_content to use less memory

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

#74 - rewrite: use a map to proof_content to use less memory

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

#73 - remove compilation warnings

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

#73 - remove compilation warnings

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

#72 - remove warnings on HOL-Light files only

Issue - State: closed - Opened by fblanqui about 1 year ago

#72 - remove warnings on HOL-Light files only

Issue - State: closed - Opened by fblanqui about 1 year ago

#71 - modify identifier renamings to handle Logic/make.ml

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

#71 - modify identifier renamings to handle Logic/make.ml

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

#70 - fix error in generated dump script

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

#70 - fix error in generated dump script

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

#69 - fix error in dump script generation

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

#69 - fix error in dump script generation

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

#68 - Opam packages for hol2dk with all dependencies (including patched HOL-Light)

Issue - State: open - Opened by MSoegtropIMC about 1 year ago - 4 comments

#68 - Opam packages for hol2dk with all dependencies (including patched HOL-Light)

Issue - State: open - Opened by MSoegtropIMC about 1 year ago - 4 comments

#67 - allow simultaneous dumping

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

#67 - allow simultaneous dumping

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

#66 - add command dump-and-simp

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

#65 - add command purge

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

#65 - add command purge

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

#64 - add another simplification rule

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

#64 - add another simplification rule

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

#63 - add command simp to simplify proof files

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

#63 - add command simp to simplify proof files

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

#62 - add script add-links

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

#62 - add script add-links

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

#61 - clarify README

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

#61 - clarify README

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

#60 - release 0.0.1

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

#60 - release 0.0.1

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

#59 - dune install files to patch HOL-Light

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

#59 - dune install files to patch HOL-Light

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

#58 - do not export unused proof steps

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

#58 - do not export unused proof steps

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

#57 - qualify Stdlib functions to avoid name clashes with HOL-Light values

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

#57 - qualify Stdlib functions to avoid name clashes with HOL-Light values

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

#56 - change dump and mk-part commands

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

#56 - change dump and mk-part commands

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

#55 - generate theorems as axioms for coq opam

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

#55 - generate theorems as axioms for coq opam

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

#54 - add clean targets in generated Makefile

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

#54 - add clean targets in generated Makefile

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

#53 - fix ci

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

#53 - fix ci

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

#52 - Reducing the size of files by eliminating intermediate steps and cuts

Issue - State: closed - Opened by thiagofelicissimo about 1 year ago - 6 comments

#52 - Reducing the size of files by eliminating intermediate steps and cuts

Issue - State: closed - Opened by thiagofelicissimo about 1 year ago - 6 comments

#51 - add mapping for usual functions on nat

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

#51 - add mapping for usual functions on nat

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

GitHub / Deducteam/hol2dk issues and pull requests