search

FStarLang / pulse

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

Add an explicit block statement #134

Open JonasAlaif opened 4 months ago

JonasAlaif commented 4 months ago

The syntax is

block
  requires ...
  ensures ...
{
  ...
}

@mtzguido no need to work on this in this PR, I created it mostly for easily seeing the diff