Merge pull request #1 from AeneasVerif/constants-v2

Implement support for globals

1 files changed, 3 insertions, 0 deletions

diff --git a/fstar/Primitives.fst b/fstar/Primitives.fst
index fe351f3a..b44fe9d1 100644
--- a/fstar/Primitives.fst
+++ b/fstar/Primitives.fst
@@ -34,6 +34,9 @@ let bind (#a #b : Type0) (m : result a) (f : a -> result b) : result b =
 // Monadic assert(...)
 let massert (b:bool) : result unit = if b then Return () else Fail
 
+// Normalize and unwrap a successful result (used for globals).
+let eval_global (#a : Type0) (x : result a{Return? (normalize_term x)}) : a = Return?.v x
+
 (*** Misc *)
 type char = FStar.Char.char
 type string = string