diff options
author | Sidney Congard | 2022-06-30 12:22:14 +0200 |
---|---|---|
committer | Sidney Congard | 2022-06-30 12:22:14 +0200 |
commit | 47691de8fe3dc32a29663d4d8343eb415ce1d81e (patch) | |
tree | 06ac570c7f9eee49987d716e043415ae31c681d0 /fstar | |
parent | da118da3e590fbea4e880121837da2ee938837f6 (diff) |
Traduct globals body separately (WIP)
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 |