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

Add missing bits for supporting default in executable specs. #814

Open
wants to merge 4 commits into
base: master
Choose a base branch
from

Conversation

yav
Copy link
Collaborator

@yav yav commented Jan 3, 2025

Fixes #813. The changes are:

  • Replace the todo exception, with a call to the relevant default function.
  • Remember to add the records from default to the record map.

Note: some future refactoring could be useful, but is not pressing, to factor out common stuff for calling default functions.

Fixes #714. This also fixes an issue in #714 where we were missing some braces. This should have been a separate PR but I accidentally pushed it here, and the change is sufficiently small that I felt it is not worth doing surgery on the repo to fix.

Fixes #813.   The changes are:

* Replace the `todo` exception, with a call to the relevant `default` function.
* Remember to add the records from `default` to the record map.

Note: some future refactoring could be useful, but is not pressing, to
factor out common stuff for calling `default` functions.
@yav yav requested a review from rbanerjee20 January 3, 2025 22:11
@septract
Copy link
Collaborator

septract commented Jan 3, 2025

This works on the instances of default in the MKM proofs, nice! I should note that we only use default as a placeholder where we need an arbitrary value of the type, which is then thrown away. So I haven't tested whether default is correctly implemented, just that cn test can handle the construct at all.

yav added 3 commits January 6, 2025 11:32
We add braces even when there is no return value.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
2 participants