Primitive weak-head reductions for declarations with iota metadata.
Summary
Types
@type fuel() :: Theoria.Normalize.Fuel.t()
@type result() :: whnf_result() | {:stuck, Theoria.Term.App.t()}
@type whnf_fun() :: (Theoria.Env.t(), Theoria.Term.t() -> whnf_result())
@type whnf_result() :: {:ok, Theoria.Term.t(), fuel()} | {:error, Theoria.Error.t()}
Functions
@spec reduce(Theoria.Env.t(), Theoria.Term.App.t(), whnf_fun()) :: result()