Theoria.Kernel.Reference.Primitive (theoria v0.4.0)

Reference primitive reductions for recursor iota metadata.

Summary

defeq_fun()

result()

whnf_fun()

Attempts one reference primitive iota reduction.

@type defeq_fun() :: (Theoria.Env.t(), Theoria.Term.t(), Theoria.Term.t() ->
                  boolean())

@type result() ::
  {:ok, Theoria.Term.t(), non_neg_integer()}
  | {:error, term()}
  | {:stuck, Theoria.Term.App.t()}

@type whnf_fun() :: (Theoria.Env.t(), Theoria.Term.t() ->
                 {:ok, Theoria.Term.t(), non_neg_integer()} | {:error, term()})

@spec reduce(Theoria.Env.t(), Theoria.Term.App.t(), whnf_fun(), defeq_fun()) ::
  result()

Attempts one reference primitive iota reduction.