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

Pretty printer - remove = from module imports with the same name #1343

Open
joscoh opened this issue Aug 6, 2021 · 0 comments
Open

Pretty printer - remove = from module imports with the same name #1343

joscoh opened this issue Aug 6, 2021 · 0 comments
Labels
kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: printer Pretty printer for Dafny's AST

Comments

@joscoh
Copy link

joscoh commented Aug 6, 2021

When generating an AliasModuleDecl and then printing it using the pretty printer (ultimately via PrintTopLevelDecls), it only seems possible to print import A = B. When we would like to say import A, this means that the resulting pretty-printed code is import A = A.

This is more cosmetic than anything else, but it would be nicer, if both sides of the import have the same name, to remove the equality from the pretty-printed version.
@keyboardDrummer keyboardDrummer added the kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny label Aug 9, 2021
@robin-aws robin-aws added the part: printer Pretty printer for Dafny's AST label Sep 1, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: printer Pretty printer for Dafny's AST
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
3 participants
@keyboardDrummer @robin-aws @joscoh