Skip to content

refactor: use the full features of mkAppM in free_union#436

Draft
eric-wieser wants to merge 1 commit intomainfrom
eric-wieser/has-fresh
Draft

refactor: use the full features of mkAppM in free_union#436
eric-wieser wants to merge 1 commit intomainfrom
eric-wieser/has-fresh

Conversation

@eric-wieser
Copy link
Collaborator

This means this will work correctly for function types with implicit and typeclass arguments

@eric-wieser
Copy link
Collaborator Author

!bench

@leanprover-radar
Copy link

leanprover-radar commented Mar 17, 2026

Benchmark results for 7d1b72d against 4f3737a are in. Significant changes detected! @eric-wieser

  • 🟥 main exited with code 1

No significant changes detected.

@chenson2018 chenson2018 self-assigned this Mar 17, 2026
@eric-wieser
Copy link
Collaborator Author

This is running into some weird elaboration trouble, which probably isn't worth looking into right now.

@eric-wieser eric-wieser marked this pull request as draft March 17, 2026 17:47
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants