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

Clean up why3 crate #108

Closed
xldenis opened this issue Oct 1, 2021 · 5 comments
Closed

Clean up why3 crate #108

xldenis opened this issue Oct 1, 2021 · 5 comments
Labels
enhancement New feature or request

Comments

@xldenis
Copy link
Collaborator

xldenis commented Oct 1, 2021

The why3 crate currently has a lot of knowledge of creusot's particular use case. I'd like to clean it up and make it a general Why3 printer / ast.
@xldenis
Copy link
Collaborator Author

xldenis commented Sep 11, 2024

This is sorely needed. I would like to see exp.rs removed / changed into a cleaner term.rs. I actually have such a refactored code in a currently private project I could probably extract.

@xldenis xldenis added the enhancement New feature or request label Sep 11, 2024
@jhjourdan
Copy link
Collaborator

@xldenis I did some cleanup in #1228. Is this enough for you?

@xldenis
Copy link
Collaborator Author

xldenis commented Nov 18, 2024

Not really, I want to completely rewrite Exp and separate it from Term (its currently a syntactic union of the two). There are similar cleanups to do in other parts I think

@jhjourdan jhjourdan mentioned this issue Nov 18, 2024
Open
@jhjourdan
Copy link
Collaborator

We no longer support Exp, I already removed the constructors which are only relevant for programs.

@jhjourdan
Copy link
Collaborator

@xldenis So can we close this issue?

@xldenis xldenis closed this as completed Nov 25, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
enhancement New feature or request
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@xldenis @jhjourdan