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

Set a limit on WHNF computation depth #187

Open
wants to merge 2 commits into
base: develop
Choose a base branch
from
Open

Conversation

fizruk
Copy link
Member

@fizruk fizruk commented Jun 11, 2024

  • Add a limit on how many nested WHNF calls are allowed
  • Default limit is 50
  • The limit can be changed in the Rzk code, for example, to set the new depth (starting at a certain point in the formalization) to 100, simply add #set-option "max-whnf-depth" = "100" at the top-level. To reset the depth to default, do #unset-option "max-whnf-depth"

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.

None yet

1 participant