Skip to content

Issues: HOL-Theorem-Prover/HOL

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

Clear current search query, filters, and sorts
95 Open 125 Closed
95 Open 125 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

add a keybinding that loads the dependencies of files for vim Editor modes Feature Request
#1470 opened Apr 25, 2025 by ordinarymath
Lie Algebra Feature Request Theories
#1365 opened Dec 8, 2024 by michael-roe
1
Theory syntax Feature Request
#1364 opened Dec 8, 2024 by digama0
9
Support definitions that are local to a theory Feature Request
#1351 opened Nov 20, 2024 by myreen
3
Port HOL Light's bitmatch to HOL4 Feature Request
#1330 opened Oct 30, 2024 by acjf3
1
Special syntax for nested/sequence of sum_CASE constants Feature Request Printing-Parsing
#1276 opened Jul 23, 2024 by mn200
Q.PAT_X_ASSUM returns bad errors Feature Request Tactics/DPs
#1230 opened May 1, 2024 by mn200
Add a q.subpat_{x_,}assum Feature Request Tactics/DPs
#1222 opened Apr 11, 2024 by mn200
Add spec form to cover both INST and SPEC of theorems Feature Request
#1221 opened Apr 11, 2024 by mn200
Tools should report config files' location Feature Request Good first issue
#1141 opened Aug 25, 2023 by mn200
Use kernel compute feature in HOL4 simplifier, decision procedures, and EVAL Feature Request
#1118 opened Jun 28, 2023 by myreen
6
Store location information about where theorems were proved in Theory.sig files Editor modes Feature Request
#1094 opened Feb 14, 2023 by mn200
qmatch_abbrev_tac should rename var/var bindings rather than abbreviate them Feature Request Tactics/DPs
#1085 opened Jan 5, 2023 by mn200
More floating point theorems Feature Request Theories
#1082 opened Dec 28, 2022 by michael-roe
3
Update Definition syntaxes to allow declaration of types of new constants Feature Request
#1065 opened Oct 26, 2022 by mn200
4
emacs-mode: have intermediate stage between all black&white, and full colouring with lots of type info Editor modes Feature Request
#1063 opened Oct 25, 2022 by mn200
Cases_on record values should use <|-|> cases theorem Feature Request Tactics/DPs
#914 opened May 16, 2021 by mn200
Pretty chained if syntax Feature Request Printing-Parsing
#890 opened Feb 12, 2021 by mn200
Auxiliary constants from datatype package Feature Request
#875 opened Nov 26, 2020 by tanyongkiam
8
Provide tactic to update an abbreviation Feature Request Tactics/DPs
#801 opened Mar 24, 2020 by mn200
rename should only affect variables Feature Request Tactics/DPs
#796 opened Mar 19, 2020 by mn200
Pattern matching in do notation Feature Request Printing-Parsing
#756 opened Nov 26, 2019 by formrre
1
Warn if modules / theories only differ by case Build/Holmake Feature Request
#679 opened Mar 19, 2019 by mn200
1
Sharing & memory consumption after theory load Feature Request Low Priority
#640 opened Jan 11, 2019 by talsewell
15
Holmakefile INCLUDES cleaner Build/Holmake Feature Request
#631 opened Dec 16, 2018 by xrchz
1
ProTip! Add no:assignee to see everything that’s not assigned.