Adding attributes to projectors, discriminators, and methods #3760
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
|
Check world was green here https://github.com/mtzguido/FStar/actions/runs/13342039658 the only failures in test-pulse are updated error locations since we also test error output. Merging. |
This makes it easy to control their normalization behavior or look all of them up in the environment. They also have qualifiers, injected by the typechecker, but these are not useful for `delta_attr` nor `delta_qual`, and are different for each individual definition, so it is impossible to do a normalization call that e.g. unfolds all projectors.
mtzguido
added a commit
to mtzguido/pulse
that referenced
this pull request
Feb 17, 2025
Lines in Prims moved after FStarLang/FStar#3760
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This makes it easy to control their normalization behavior or look all
of them up in the environment. They also have qualifiers, injected
by the typechecker, but these are not useful for
delta_attrnordelta_qual, and are different for each individual definition, so it isimpossible to do a normalization call that e.g. unfolds all projectors.