Skip to content
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

refactor: extract handling of RecForms #38

Merged
merged 1 commit into from
Aug 17, 2024

Conversation

Equilibris
Copy link
Collaborator

@Equilibris Equilibris commented Aug 16, 2024

There is a piece of functionality that was created for Ind.lean, this turns out to be useful at other points throughout the code, we extract this to its own file in this PR.

Additionally to this, we uncomment the line concealing the composed recursive form and add handles to throw errors if it is found. This is due to it being required in DeepThunk constructor generation.

This PR is non functional.

@Equilibris Equilibris requested a review from alexkeizer as a code owner August 16, 2024 09:57
Copy link
Contributor

@AtticusKuhn AtticusKuhn left a comment

Choose a reason for hiding this comment

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

This seems like a pretty simple change. Looks good to me.

Copy link
Owner

@alexkeizer alexkeizer left a comment

Choose a reason for hiding this comment

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

LGTM

@Equilibris Equilibris merged commit 2960ed4 into master Aug 17, 2024
2 checks passed
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