val op_let_Plus (#a #b: Type) (x: possibly a) (f: (a -> possibly b)) : possibly b
let (let+) (#a #b:Type) (x:possibly a) (f:a -> possibly b) : possibly b =
  match x with
  | Err s -> Err s
  | Ok x' -> f x'
val op_let_Plus (#a #b: Type) (x: possibly a) (f: (a -> possibly b)) : possibly b
let op_let_Plus (#a #b: Type) (x: possibly a) (f: (a -> possibly b)) : possibly b =
match x with
| Err s -> Err s
| Ok x' -> f x'
Vale.Def.PossiblyMonad.fst.checked
prims.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.Classical.fsti.checked
Vale.Def.PossiblyMonad.fst
Vale.Def.PossiblyMonad.possibly Prims.string Vale.Def.PossiblyMonad.Err
module Vale.Def.PossiblyMonad

/// Similar to the [maybe] monad in Haskell (which is like the
/// [option] type in F* and OCaml), but instead, we also store the
/// reason for the error when the error occurs.

type possibly 'a =
  | Ok : v:'a -> possibly 'a
  | Err : reason:string -> possibly 'a

unfold let return (#a:Type) (x:a) : possibly a =
  Ok x
val op_let_Plus (#a #b: Type) (x: possibly a) (f: (a -> possibly b)) : possibly b
x: Vale.Def.PossiblyMonad.possibly a -> f: (_: a -> Vale.Def.PossiblyMonad.possibly b)
  -> Vale.Def.PossiblyMonad.possibly b