Library FreeSpec.Exec.Eval

From FreeSpec Require Import Core.

Inductive EVAL (a : Type) : Type :=
| Eval (x : a) : EVAL a.

Arguments Eval [a] (x).

Definition eval `{Provide ix EVAL} {a} (x : a) : impure ix a :=
  request (Eval x).

Register EVAL as freespec.exec.eval.type.
Register Eval as freespec.exec.eval.Eval.