Control.RIO.State

Definitions

record Read : l -> Type -> Type

  Effectful getter, yielding values of type `a` and tagged
  with label `lbl`.

Totality: total
Visibility: public export
Constructor: 

MkRead : IO a -> Read lbl a

Projection: 

.read : HasIO io => Read lbl a -> io a

  Read the current value of a getter.
  
  Use this if you experience slowdowns with `readAt` durcing compilation.

Hint: 

ST lbl a => Read lbl a

readAt : (0 lbl : l) -> Read lbl a => HasIO io => io a

  Read the current value of a getter.

Totality: total
Visibility: export

.read : HasIO io => Read lbl a -> io a

  Read the current value of a getter.
  
  Use this if you experience slowdowns with `readAt` durcing compilation.

Totality: total
Visibility: export

data ST : l -> Type -> Type

  Mutable state holding values of type `a` and tagged
  with label `lbl`.

Totality: total
Visibility: public export
Constructor: 

MkST : IO a -> (a -> IO ()) -> ((a -> a) -> IO ()) -> ST lbl a

Hint: 

ST lbl a => Read lbl a

mkST : HasIO io => a -> io (ST lbl a)

Totality: total
Visibility: export

stToRead : ST lbl a => Read lbl a

Totality: total
Visibility: export

mapST : (a -> b) -> (b -> a -> a) -> ST lbl a -> ST lbl2 b

  Viewing a mutable state through a getter and a setter.

Totality: total
Visibility: export

modifyAt : (0 lbl : l) -> ST lbl a => HasIO io => (a -> a) -> io ()

  Modify the value stored in a mutable reference.

Totality: total
Visibility: export

getAt : (0 lbl : l) -> ST lbl a => HasIO io => io a

  Write a value to a mutable reference.

Totality: total
Visibility: export

setAt : (0 lbl : l) -> ST lbl a => HasIO io => a -> io ()

  Write a value to a mutable reference.

Totality: total
Visibility: export

.get : HasIO io => ST lbl a -> io a

  Read the current value of some mutable state.
  
  Use this if you experience slowdowns with `getAt` durcing compilation.

Totality: total
Visibility: export

.set : HasIO io => ST lbl a -> a -> io ()

  Overwrite the current value of some mutable state.
  
  Use this if you experience slowdowns with `setAt` durcing compilation.

Totality: total
Visibility: export

.mod : HasIO io => ST lbl a -> (a -> a) -> io ()

  Modify the current value of some mutable state.
  
  Use this if you experience slowdowns with `setAt` durcing compilation.

Totality: total
Visibility: export
Fixity Declaration: infixl operator, level 9