diff options
| author | Son Ho | 2023-01-13 21:44:26 +0100 |
|---|---|---|
| committer | Son HO | 2023-02-03 11:21:46 +0100 |
| commit | 71863baf896d0f6c07473fce16e7568aa39064bc (patch) | |
| tree | 9b3e3c2143c38e3a1b1ead64c315781c23ef4524 /backends | |
| parent | 5eca1a621a6446dfc3e5e63e76f4f810ece9c6e3 (diff) | |
Do not unfold the monadic lets for the generated F* code
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 |