diff options
Diffstat (limited to 'fstar/Primitives.fst')
| -rw-r--r-- | fstar/Primitives.fst | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/fstar/Primitives.fst b/fstar/Primitives.fst index b8da70c4..46fa2d87 100644 --- a/fstar/Primitives.fst +++ b/fstar/Primitives.fst @@ -9,6 +9,16 @@ 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;` +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 + | Return x -> f x + | Fail -> Fail + +// Monadic assert(...) +let massert (b:bool) : result unit = if b then Return () else Fail + (*** Misc *) type char = FStar.Char.char |