search

FStarLang / steel

The Steel separation logic library for F*
Apache License 2.0
31 stars 5 forks source link

More support for unobservable #152

Closed mtzguido closed 9 months ago

mtzguido commented 9 months ago

This PR allows to annotate functions as unobservable, like for atomic and ghost already, and makes the checker lift from unobservable to atomic when needed.

mtzguido commented 9 months ago

cc @nikswamy