@[reducible, inline]

abbrev Control.Monad.Reader.Reader (ρ α : Type) : Type

The Reader monad: ReaderT over Id.

$$\text{Reader}\ \rho\ \alpha = \text{ReaderT}\ \rho\ \text{Id}\ \alpha = \rho \to \alpha$$

Equations

• Control.Monad.Reader.Reader ρ α = ReaderT ρ Id α

@[inline]

def Control.Monad.Reader.ask {m : Type u_1 → Type u_2} {ρ : Type u_1} [Monad m] : ReaderT ρ m ρ

Read the environment.

$$\text{ask} : \text{ReaderT}\ \rho\ m\ \rho$$

Alias for Lean's read.

Equations

• Control.Monad.Reader.ask = read

@[inline]

def Control.Monad.Reader.asks {m : Type u_1 → Type u_2} {ρ α : Type u_1} [Monad m] (f : ρ → α) : ReaderT ρ m α

Project a function over the environment.

$$\text{asks}(f) = f \circ \text{ask}$$

Equivalent to f <$> ask.

Equations

• Control.Monad.Reader.asks f = f <$> read

@[inline]

def Control.Monad.Reader.local {ρ : Type u_1} {m : Type u_1 → Type u_2} {α : Type u_1} (f : ρ → ρ) (ma : ReaderT ρ m α) : ReaderT ρ m α

Run a computation in a modified environment.

$$\text{local}(f, ma) : \text{ReaderT}\ \rho\ m\ \alpha$$

Runs ma with the environment transformed by f. Alias for Lean's ReaderT.adapt.

Equations

• Control.Monad.Reader.local f ma = ReaderT.adapt f ma

@[inline]

def Control.Monad.Reader.runReaderT {ρ : Type u_1} {m : Type u_1 → Type u_2} {α : Type u_1} (ma : ReaderT ρ m α) (env : ρ) : m α

Run a ReaderT computation with a given environment.

$$\text{runReaderT}(ma, \rho) : m\ \alpha$$

Alias for ReaderT.run.

Equations

• Control.Monad.Reader.runReaderT ma env = ma.run env

@[inline]

def Control.Monad.Reader.runReader {ρ α : Type} (ma : Reader ρ α) (env : ρ) : α

Run a Reader computation with a given environment.

$$\text{runReader}(ma, \rho) : \alpha$$

Equations

• Control.Monad.Reader.runReader ma env = ReaderT.run ma env

@[inline]

def Control.Monad.Reader.mapReaderT {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} {ρ α β : Type u_1} (f : m α → n β) (ma : ReaderT ρ m α) : ReaderT ρ n β

Map over the inner monadic computation.

$$\text{mapReaderT}(f, ma) : \text{ReaderT}\ \rho\ n\ \beta$$

where $f : m\ \alpha \to n\ \beta$.

Equations

• Control.Monad.Reader.mapReaderT f ma env = f (ma.run env)

theorem Control.Monad.Reader.ask_run {m : Type u_1 → Type u_2} {ρ : Type u_1} [Monad m] (env : ρ) : runReaderT ask env = pure env

ask returns the environment: runReaderT ask env = pure env. $$\text{runReaderT}(\text{ask}, \rho) = \text{pure}(\rho)$$

theorem Control.Monad.Reader.local_id {ρ : Type u_1} {m : Type u_1 → Type u_2} {α : Type u_1} (ma : ReaderT ρ m α) : «local» id ma = ma

local id is identity: does not change the computation. $$\text{local}(\text{id}, ma) = ma$$

theorem Control.Monad.Reader.runReader_pure {α ρ : Type} (a : α) (env : ρ) : runReader (pure a) env = a

runReader of pure a returns a. $$\text{runReader}(\text{pure}\ a, \rho) = a$$