open Preamble

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open Jmeq

open Russell

open Bool

open Nat

open List

open Setoids

open Relations

open Monad

(** val option : Monad.monadProps **)
let option =
  Monad.makeMonadProps (fun _ x -> Types.Some x) (fun _ _ m f ->
    match m with
    | Types.None -> Types.None
    | Types.Some x -> f x)

(** val opt_safe : 'a1 Types.option -> 'a1 **)
let opt_safe m =
  (match m with
   | Types.None -> (fun _ -> Logic.false_rect_Type0 __)
   | Types.Some t -> (fun _ -> t)) __

(** val opt_try_catch : 'a1 Types.option -> (Types.unit0 -> 'a1) -> 'a1 **)
let opt_try_catch m f =
  match m with
  | Types.None -> f Types.It
  | Types.Some x -> x

(** val optPred : Monad.injMonadPred **)
let optPred =
  { Monad.im_pred = Monad.Mk_MonadPred; Monad.mp_inject = (fun _ _ m_sig ->
    let m = m_sig in
    (match Obj.magic m with
     | Types.None -> (fun _ -> Obj.magic Types.None)
     | Types.Some x -> (fun _ -> Obj.magic (Types.Some x))) __) }