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
Copy Markdown
Collaborator

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

@eric-wieser
Copy link
Copy Markdown
Collaborator Author

!bench

@leanprover-radar
Copy link
Copy Markdown

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
Copy Markdown
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

3 participants