Section Reader.

Variable (Env : Type).

Variant readerE : Type -> Type :=
| Ask : readerE Env.

Definition ask {E F} `{readerE +? F -< E} : itree E Env :=
  trigger Ask.

Definition eval_reader {E} : Env -> Handler readerE E :=
  fun r _ e =>
    match e with
    | Ask => Ret r
    end.

Definition run_reader {E F} `{readerE +? E -< F} : Env -> itree F ~> itree E :=
  fun r => interp (T := fun x => x) (over (eval_reader r)).

End Reader.

Arguments ask {Env E F _}.
Arguments run_reader {Env E F _} _ _ _.