val fail_with (#a: Type) (s: string) : possibly a
let fail_with (#a:Type) (s:string) : possibly a = Err s
val fail_with (#a: Type) (s: string) : possibly a
let fail_with (#a: Type) (s: string) : possibly a =
Err s
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
Prims.string Vale.Def.PossiblyMonad.Err Vale.Def.PossiblyMonad.possibly
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

unfold 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 fail_with (#a: Type) (s: string) : possibly a
s: Prims.string -> Vale.Def.PossiblyMonad.possibly a