-
-
Notifications
You must be signed in to change notification settings - Fork 369
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.
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
Allow hole filling to deal with recursion #472
Conversation
This changes the heuristics so we get a reasonable fmap @[], but breaks note.
I was forgetting to count destruct as usage
…nguage-server into recursion-frame-wtf
Realized there's more infrastructure work I want to do here before merging. Can't figure out how to turn it into a draft PR, sorry. |
(thanks to @i-am-tom for the idea!)
I made it a draft, there was a thing on the top right, near where you add reviewers. It looks like plain text, but is clickable |
@WorldSEnder would love to have you on board! Feel free to reach out to me (fpslack: isovector, email: [email protected]) if you're interested in helping. |
Tactic tracing
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I dont know the tactic plugin code enough to do a proper review but trusting yours 😃
@TOTBWF and I are back with more! This PR enhances the "attempt to fill hole" code action, allowing it to implement self-recursive functions. The generated code ensures recursion occurs only on structurally-smaller values, and preserves the positional ordering of homomorphically destructed arguments.
It's clever enough to implement
foldr
:and nontrivial functor instances: