From 71863baf896d0f6c07473fce16e7568aa39064bc Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 13 Jan 2023 21:44:26 +0100
Subject: Do not unfold the monadic lets for the generated F* code

---
 backends/fstar/Primitives.fst | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'backends/fstar')

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
-- 
cgit v1.2.3