diff options
author | Son Ho | 2022-02-07 10:39:47 +0100 |
---|---|---|
committer | Son Ho | 2022-02-07 10:39:47 +0100 |
commit | 0db8e292dc9a0e653eae8c2113859f41729faab3 (patch) | |
tree | 38123284b4edf29f00f9b78976c46e147f897120 /fstar | |
parent | 4f116135d0c5abe98aaa763664c7ac33a7084c36 (diff) |
Make more minor modifications
Diffstat (limited to 'fstar')
-rw-r--r-- | fstar/Primitives.fst | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/fstar/Primitives.fst b/fstar/Primitives.fst index dae73f46..6b1ec539 100644 --- a/fstar/Primitives.fst +++ b/fstar/Primitives.fst @@ -9,7 +9,9 @@ type result (a : Type0) : Type0 = | Return : a -> result a | Fail : result a -// Monadic bind and return (allows us to use the monadic notations like `y <-- f x;` +// Monadic bind and return. +// Re-definining those allows us to customize the result of the monadic notations +// like: `y <-- f x;` let return (#a : Type0) (x:a) : result a = Return x let bind (#a #b : Type0) (m : result a) (f : a -> result b) : result b = match m with |