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
27 Open 73 Closed
27 Open 73 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
Assigned to nobody Loading
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Issues list

Pretty-printing of quantified formula is gross Bug Printing-Parsing
#1361 opened Dec 4, 2024 by mn200
@mn200
Special syntax for nested/sequence of sum_CASE constants Feature Request Printing-Parsing
#1276 opened Jul 23, 2024 by mn200
Case expression prints badly Bug Printing-Parsing
#1086 opened Jan 10, 2023 by mn200
1
Pretty chained if syntax Feature Request Printing-Parsing
#890 opened Feb 12, 2021 by mn200
Allow definition labels to replace conjunctions Low Priority Printing-Parsing
#876 opened Dec 4, 2020 by mn200
Pattern matching in do notation Feature Request Printing-Parsing
#756 opened Nov 26, 2019 by formrre
1
Add option to print brackets explicitly instead of relying on operator precedence Feature Request Printing-Parsing
#628 opened Dec 13, 2018 by formrre
Bad type error message in presence of overloading Feature Request Printing-Parsing
#617 opened Nov 27, 2018 by mn200
1
Better syntax for chained updates to functions and finite maps Feature Request Printing-Parsing
#616 opened Nov 23, 2018 by mn200
2
Add tooltip type information to record fields Feature Request Printing-Parsing
#589 opened Sep 18, 2018 by mn200
Restricted quantifier pretty-printing failure Bug Printing-Parsing
#532 opened May 1, 2018 by mn200
Error messages when type-checking case expressions are disgusting Feature Request Printing-Parsing
#517 opened Feb 22, 2018 by mn200
Consider inverting sense of parenthesis-style directive ParoundPrec Printing-Parsing
#486 opened Oct 25, 2017 by mn200
2
Warn when record literal omits fields Feature Request Printing-Parsing
#364 opened Sep 29, 2016 by mn200
Report line numbers associated with (non-parsing) HOL_ERRs Low Priority Printing-Parsing
#354 opened Jun 29, 2016 by mn200
Possible pretty-printing overload issue Printing-Parsing
#240 opened Mar 3, 2015 by mn200
Install monad syntax by default Feature Request Good first issue Printing-Parsing
#211 opened Nov 20, 2014 by mn200
math mode munger plays badly with inference rules Printing-Parsing
#177 opened Jul 24, 2014 by xrchz
Tidy up modularisation in Hol_pp and DB. Feature Request Low Priority Printing-Parsing
#133 opened Nov 3, 2013 by mn200
analogue of overload_info_for for types Printing-Parsing
#124 opened Jul 1, 2013 by xrchz
Binder-like syntax for {PROD,SUM}_IMAGE Feature Request Printing-Parsing
#51 opened Jan 11, 2012 by mn200
@mn200
1
New syntax for function-valued fields Feature Request Low Priority Printing-Parsing
#33 opened Oct 4, 2011 by mn200
Syntax for list comprehensions Feature Request Printing-Parsing
#26 opened Oct 3, 2011 by mn200
3
Allow specification of grammar to LaTeX munger commands Feature Request Printing-Parsing
#22 opened Sep 19, 2011 by mn200
@mn200
Allow 'raw' option to LaTeX munger commands Feature Request Printing-Parsing
#21 opened Sep 19, 2011 by mn200
@mn200
ProTip! Find all open issues with in progress development work with linked:pr.