val return (#a: Type) (x: a) : possibly a
let return (#a:Type) (x:a) : possibly a =
  Ok x
val return (#a: Type) (x: a) : possibly a
let return (#a: Type) (x: a) : possibly a =
Ok 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.Ok 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
val return (#a: Type) (x: a) : possibly a
x: a -> Vale.Def.PossiblyMonad.possibly a