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

val state_get : 'a1 Monad.smax_def__o__monad

val state_set : 'a1 -> Types.unit0 Monad.smax_def__o__monad

val state_run : 'a1 -> 'a2 Monad.smax_def__o__monad -> 'a2

val state_update : ('a1 -> 'a1) -> Types.unit0 Monad.smax_def__o__monad

val state_pred : Monad.monadPred

val stateRel : Monad.monadRel