Skip to content

Ltac2, Message.empty #20392

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
Open
patrick-nicodemus opened this issue Mar 25, 2025 · 4 comments
Open

Ltac2, Message.empty #20392

patrick-nicodemus opened this issue Mar 25, 2025 · 4 comments
Labels
good first issue Beginners welcome to submit a pull request. kind: wish Feature or enhancement requests. part: ltac2 Issues and PRs related to the (in development) Ltac2 tactic langauge.

Comments

@patrick-nicodemus
Copy link
Contributor

Is your feature request related to a problem?

This is just a suggestion, but I think concatenating a list of messages with List.fold_left Message.concat (Message.of_string "") msglist would look a little nicer if there was a dedicated Message.empty constant which is defined to be a left/right unit for concat.

Proposed solution

No response

Alternative solutions

No response

Additional context

No response
@patrick-nicodemus patrick-nicodemus added kind: wish Feature or enhancement requests. needs: triage The validity of this issue needs to be checked, or the issue itself updated. labels Mar 25, 2025
@SkySkimmer SkySkimmer added part: ltac2 Issues and PRs related to the (in development) Ltac2 tactic langauge. good first issue Beginners welcome to submit a pull request. and removed needs: triage The validity of this issue needs to be checked, or the issue itself updated. labels Mar 25, 2025
@SkySkimmer
Copy link
Contributor

Feel free to make a PR.

@patrick-nicodemus
Copy link
Contributor Author

Thank you! I will give it a shot.

@gperdutoutmoncodetipe
Copy link

Hi,

I'm new to open source and this issue looks approachable to me.
Would it be okay if I gave it a try, as long as no one has started working on it yet, @patrick-nicodemus?

Thanks!

@patrick-nicodemus
Copy link
Contributor Author

@gperdutoutmoncodetipe You're welcome to start working on it. I have not done anything with it yet.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
good first issue Beginners welcome to submit a pull request. kind: wish Feature or enhancement requests. part: ltac2 Issues and PRs related to the (in development) Ltac2 tactic langauge.
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
3 participants
@SkySkimmer @patrick-nicodemus @gperdutoutmoncodetipe