search

FStarLang / pulse

The Pulse separation logic DSL for F*
Apache License 2.0
6 stars 7 forks source link

Fix ensures annotations on with_invariants #140

Closed aseemr closed 4 months ago

aseemr commented 4 months ago

The PR fixes the pulse checker so that the with_invariants ensures can be annotated just as p frame, as opposed to inv i p frame.