diff options
Diffstat (limited to 'fstar')
| -rw-r--r-- | fstar/Primitives.fst | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/fstar/Primitives.fst b/fstar/Primitives.fst index fe351f3a..b3da25c2 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 +// Unwrap a successful result by normalisation (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 |