Skip to content
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

Jump to bottom

Short names are not used for printing Theorems #1607

Open
brianhuffman opened this issue Mar 9, 2022 · 0 comments
Open

Short names are not used for printing Theorems #1607

brianhuffman opened this issue Mar 9, 2022 · 0 comments
Labels
subsystem: saw-core Issues related to the saw-core representation or the saw-core subsystem type: enhancement Issues describing an improvement to an existing feature or capability usability An issue that impedes efficient understanding and use
Milestone
2025T1

Comments

@brianhuffman
Copy link
Contributor

When printing a Theorem value (e.g. something proved with prove_print) with the saw-script print command, the pretty-printer does not display the preferred short names for constants; instead it prints the fully-qualified URI form of all names.

We should fix this so that it displays the more readable short names.

This is closely related to #1277.
@brianhuffman brianhuffman mentioned this issue Mar 9, 2022
Open
@sauclovian-g sauclovian-g added type: enhancement Issues describing an improvement to an existing feature or capability usability An issue that impedes efficient understanding and use subsystem: saw-core Issues related to the saw-core representation or the saw-core subsystem labels Nov 2, 2024
@sauclovian-g sauclovian-g added this to the 2025T1 milestone Nov 2, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
subsystem: saw-core Issues related to the saw-core representation or the saw-core subsystem type: enhancement Issues describing an improvement to an existing feature or capability usability An issue that impedes efficient understanding and use
Projects
None yet
Milestone
2025T1
Development

No branches or pull requests
2 participants
@brianhuffman @sauclovian-g