diff options
| author | Sidney Congard | 2022-07-05 12:16:36 +0200 |
|---|---|---|
| committer | Sidney Congard | 2022-07-05 12:16:36 +0200 |
| commit | eebedf86db68c240fe16cfd74af2cc462b0d9cf9 (patch) | |
| tree | e79facc5aa78c213e224559bc4dd39442f1fab1c /tests/betree/Primitives.fst | |
| parent | fdbbb82ff89b1d5141ec63bc2385936da3de3616 (diff) | |
Remove last prints, adapt JSON
Diffstat (limited to '')
| -rw-r--r-- | tests/betree/Primitives.fst | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/tests/betree/Primitives.fst b/tests/betree/Primitives.fst index fe351f3a..b3da25c2 100644 --- a/tests/betree/Primitives.fst +++ b/tests/betree/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 |