open Preamble

open Jmeq

open Russell

open Bool

open Nat

open List

open Setoids

open Relations

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open Monad

(** val state_monad : Monad.setoidMonadProps **)
let state_monad =
  Monad.makeSetoidMonadProps (fun _ x s -> { Types.fst = s; Types.snd = x })
    (fun _ _ m f s -> let { Types.fst = s'; Types.snd = x } = m s in f x s')

(** val state_get : 'a1 Monad.smax_def__o__monad **)
let state_get =
  Obj.magic (fun s -> { Types.fst = s; Types.snd = s })

(** val state_set : 'a1 -> Types.unit0 Monad.smax_def__o__monad **)
let state_set s =
  Obj.magic (fun x -> { Types.fst = s; Types.snd = Types.It })

(** val state_run : 'a1 -> 'a2 Monad.smax_def__o__monad -> 'a2 **)
let state_run s c =
  (Obj.magic c s).Types.snd

(** val state_update :
    ('a1 -> 'a1) -> Types.unit0 Monad.smax_def__o__monad **)
let state_update f =
  Obj.magic (fun s -> { Types.fst = (f s); Types.snd = Types.It })

(** val state_pred : Monad.monadPred **)
let state_pred =
  Monad.Mk_MonadPred

(** val stateRel : Monad.monadRel **)
let stateRel =
  Monad.Mk_MonadRel