search

FStarLang / FStar

A Proof-oriented Programming Language
https://fstar-lang.org
Apache License 2.0
2.7k stars 234 forks source link

Sealed: mark seal/unseal as coercions #3465

Open mtzguido opened 2 months ago

mtzguido commented 2 months ago

Draft, should test across projects.

TWal commented 2 months ago

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

mtzguido commented 2 months ago

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 https://github.com/FStarLang/FStar/pull/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 commented 2 months ago

Ah excellent, thank you!