Section Reader.

Variable (Env : Type).

Variant readerE : Type → Type :=
| Ask : readerE Env.

Definition ask {E} `{readerE -< 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} : Env → itree (readerE +' E) ~> itree E :=
  fun r ⇒ interp (case_ (eval_reader r) (id_ _)).

End Reader.

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