diff options
Diffstat (limited to '')
| -rw-r--r-- | tests/betree/Primitives.fst | 2 | ||||
| -rw-r--r-- | tests/hashmap/Primitives.fst | 2 | ||||
| -rw-r--r-- | tests/hashmap_on_disk/Primitives.fst | 2 | ||||
| -rw-r--r-- | tests/misc/Primitives.fst | 2 |
4 files changed, 4 insertions, 4 deletions
diff --git a/tests/betree/Primitives.fst b/tests/betree/Primitives.fst index b3da25c2..b44fe9d1 100644 --- a/tests/betree/Primitives.fst +++ b/tests/betree/Primitives.fst @@ -34,7 +34,7 @@ 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). +// 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 *) diff --git a/tests/hashmap/Primitives.fst b/tests/hashmap/Primitives.fst index b3da25c2..b44fe9d1 100644 --- a/tests/hashmap/Primitives.fst +++ b/tests/hashmap/Primitives.fst @@ -34,7 +34,7 @@ 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). +// 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 *) diff --git a/tests/hashmap_on_disk/Primitives.fst b/tests/hashmap_on_disk/Primitives.fst index b3da25c2..b44fe9d1 100644 --- a/tests/hashmap_on_disk/Primitives.fst +++ b/tests/hashmap_on_disk/Primitives.fst @@ -34,7 +34,7 @@ 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). +// 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 *) diff --git a/tests/misc/Primitives.fst b/tests/misc/Primitives.fst index b3da25c2..b44fe9d1 100644 --- a/tests/misc/Primitives.fst +++ b/tests/misc/Primitives.fst @@ -34,7 +34,7 @@ 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). +// 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 *) |