Skip to content

fix: trait items must be rendered along with the generic params#1813

Merged
abentkamp merged 2 commits intomainfrom
fix-trait-item
Dec 16, 2025
Merged

fix: trait items must be rendered along with the generic params#1813
abentkamp merged 2 commits intomainfrom
fix-trait-item

Conversation

@abentkamp
Copy link
Copy Markdown
Contributor

@abentkamp abentkamp commented Dec 16, 2025

@abentkamp abentkamp added this to the Lean backend v1.0 milestone Dec 16, 2025
@abentkamp abentkamp requested a review from W95Psp December 16, 2025 07:54
@abentkamp abentkamp requested a review from a team as a code owner December 16, 2025 07:54
@abentkamp abentkamp added bug Something isn't working backend Issue in one of the backends (i.e. F*, Coq, EC...) lean Related to the Lean backend or library labels Dec 16, 2025
Copy link
Copy Markdown
Contributor

@W95Psp W95Psp left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM, thanks!

@abentkamp abentkamp enabled auto-merge December 16, 2025 09:09
@abentkamp abentkamp added this pull request to the merge queue Dec 16, 2025
github-merge-queue bot pushed a commit that referenced this pull request Dec 16, 2025
fix: trait items must be rendered along with the generic params
@github-merge-queue github-merge-queue bot removed this pull request from the merge queue due to failed status checks Dec 16, 2025
@abentkamp abentkamp added this pull request to the merge queue Dec 16, 2025
Merged via the queue into main with commit d4fc12f Dec 16, 2025
17 of 18 checks passed
@abentkamp abentkamp deleted the fix-trait-item branch December 16, 2025 10:39
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

backend Issue in one of the backends (i.e. F*, Coq, EC...) bug Something isn't working lean Related to the Lean backend or library

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants