diff options
Diffstat (limited to 'backends')
| -rw-r--r-- | backends/fstar/Primitives.fst | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/backends/fstar/Primitives.fst b/backends/fstar/Primitives.fst index bf0f9078..98a696b6 100644 --- a/backends/fstar/Primitives.fst +++ b/backends/fstar/Primitives.fst @@ -35,7 +35,9 @@ unfold let return (#a : Type0) (x : a) : result a = Return x // let* x = y in // ... // ``` -unfold let (let*) (#a #b : Type0) (m: result a) (f: a -> result b) : result b = +unfold let (let*) (#a #b : Type0) (m: result a) + (f: (x:a) -> Pure (result b) (requires (m == Return x)) (ensures fun _ -> True)) : + result b = match m with | Return x -> f x | Fail e -> Fail e |