diff options
| author | Son HO | 2022-09-22 16:35:29 +0200 |
|---|---|---|
| committer | GitHub | 2022-09-22 16:35:29 +0200 |
| commit | 6b6bbb9fcd56501b4f6ab1c6c16b9878a49aaadd (patch) | |
| tree | a26ed1f94e30495c43840155025cf9361a8d8a4a | |
| parent | 573dc89a52224be4c0887ae98d677305605b0539 (diff) | |
Update fstar/Primitives.fst
| -rw-r--r-- | fstar/Primitives.fst | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/fstar/Primitives.fst b/fstar/Primitives.fst index b3da25c2..b44fe9d1 100644 --- a/fstar/Primitives.fst +++ b/fstar/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 *) |