Skip to content

Issues: jrh13/hol-light

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

46 Open 9 Closed
46 Open 9 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Assignee
Filter by who’s assigned
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Issues list

Benign redefinition does not happen if there are multiple clauses
#121 opened Dec 1, 2024 by aqjune-aws
Nearly additive or multiplicative ?
#112 opened Sep 25, 2024 by fblanqui
2
No release - and none with OCaml 5 support
#101 opened Jun 20, 2024 by SnarkBoojum
11
How to use Map.Make after "hol.ml"?
#73 opened Jan 16, 2023 by fblanqui
3
HOL-Light with recent versions of ocaml & camlp5 ?
#72 opened Jan 16, 2023 by fblanqui
5
HOL Terminal Basic Issues, Syntax and Related Commands
#70 opened Sep 30, 2022 by jjoneslivingstone
4
instantiate can produce terms that are not parsable
#68 opened Jun 8, 2022 by htzh
1
opam installation
#67 opened May 8, 2022 by ncihnegn
3
HOL light installation problem on macos
#66 opened Oct 14, 2021 by dcr2828
6
[INFO] HOL Light Native
#65 opened Aug 19, 2021 by htzh
1
make error
#64 opened Jun 30, 2021 by wdmjun
5
unable to install hol-light on mac or centos 7.4
#62 opened Apr 18, 2021 by yunjiangster
Illegal begin of top_parse
#60 opened Oct 11, 2020 by AI-coder
1
"Comms::Receive failed" when inference the whole val dataset to generate proof_log
#59 opened Jul 22, 2020 by zhou745
Forum for HOL Light questions, collaborations etc
#55 opened Oct 22, 2019 by brando90
5
Installing for Apple/Mac's Unix
#54 opened Jun 2, 2019 by brando90
6
(Maybe) a typo in Examples/prog.ml ?
#43 opened Feb 21, 2018 by zidongtuili
Missing flyspeck cong
#31 opened Dec 22, 2016 by ghost
Error on the installation: Cannot find file camlp5o.cma
#29 opened Dec 11, 2016 by asr
1
running example error when using tactics g
#27 opened Jun 7, 2016 by hoyeunglee
1
Examples/prog.ml: VC_TAC has trouble with with single-variable programs auto-migrated Priority-Medium Type-Defect
#26 opened Oct 19, 2015 by GoogleCodeExporter
1
Camlp5-6.12 is out auto-migrated Priority-Medium Type-Defect
#25 opened Oct 19, 2015 by GoogleCodeExporter
3
Documentation update from HOL4: GEN_REWRITE_TAC auto-migrated Priority-Medium Type-Defect
#24 opened Oct 19, 2015 by GoogleCodeExporter
1
Typos in documentation of 'injectivity' and 'distinctness' auto-migrated Priority-Medium Type-Defect
#23 opened Oct 19, 2015 by GoogleCodeExporter
1
Minor grammar issues in help auto-migrated Priority-Medium Type-Defect
#22 opened Oct 19, 2015 by GoogleCodeExporter
2
ProTip! no:milestone will show everything without a milestone.