search

FStarLang / pulse

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

Assume (pure part of) pre in typechecking post #179

Open mtzguido opened 2 months ago

mtzguido commented 2 months ago

It would be great if this worked

assume val pre : nat -> slprop

fn setup (x:int)
  requires pure (x >= 0)
  ensures  pre x

It is essentially https://github.com/FStarLang/FStar/issues/57 for Pulse.