Skip to content

Sealed: mark seal/unseal as coercions#3465

Draft
mtzguido wants to merge 1 commit into
FStarLang:masterfrom
mtzguido:seal
Draft

Sealed: mark seal/unseal as coercions#3465
mtzguido wants to merge 1 commit into
FStarLang:masterfrom
mtzguido:seal

Conversation

@mtzguido
Copy link
Copy Markdown
Member

Draft, should test across projects.

@TWal
Copy link
Copy Markdown
Contributor

TWal commented Sep 11, 2024

I didn't know [@@coercion]! What is it doing?

@mtzguido
Copy link
Copy Markdown
Member Author

Hi Théophile, sorry, I now realize we didn't have any documentation on them. I started a doc/ref directory where I will place notes about this kind of features (which may not be polished enough for the book). Adding them here #3484, including a note about coercions.

This made me realize these coercions will probably not work so well either, since they are usually not between named types.

@TWal
Copy link
Copy Markdown
Contributor

TWal commented Sep 17, 2024

Ah excellent, thank you!

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.

2 participants