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

Fix a bug related to hide/reveal and recursive functions #5764

Merged
merged 4 commits into from
Sep 12, 2024

Conversation

keyboardDrummer
Copy link
Member

@keyboardDrummer keyboardDrummer commented Sep 11, 2024

Fixes #5763

Description

  • No longer allow hiding functions from the Dafny prelude by using hide *. This affected recursive functions because they use $LS which is defined in the prelude.

How has this been tested?

  • Added a CLI test-case to revealFunctions.dfy

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

@keyboardDrummer keyboardDrummer changed the title Reveal recursive functions Fix a bug related to hide/reveal and recursive functions Sep 11, 2024
MikaelMayer
MikaelMayer previously approved these changes Sep 12, 2024
Copy link
Member

@MikaelMayer MikaelMayer left a comment

Choose a reason for hiding this comment

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

Looks great !

@keyboardDrummer keyboardDrummer merged commit dc44321 into dafny-lang:master Sep 12, 2024
22 checks passed
@keyboardDrummer keyboardDrummer deleted the revealRecursive branch September 12, 2024 15:29
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.

hide statements don't work with recursive functions defined in different modules
2 participants