Experimental/internal API for 0.2; subject to change before 0.3. Tiny untrusted simplification groundwork backed by generated equation rules.
Summary
Functions
Normalizes a term, realizes the equality proof, and installs it under a user declaration name.
Repeatedly applies generated equation simplifications until normal form or fuel exhaustion.
Applies one generated equation simplification, if possible.
Normalizes and realizes the produced equality as a checked artifact.
Types
@type result() :: Theoria.Simp.Result.t()
Functions
@spec add_theorem(Theoria.Env.t(), atom(), Theoria.Term.t(), keyword()) :: {:ok, Theoria.Env.t(), Theoria.Theorem.t()} | {:error, term()}
Normalizes a term, realizes the equality proof, and installs it under a user declaration name.
@spec normalize(Theoria.Env.t(), Theoria.Term.t(), keyword()) :: result()
Repeatedly applies generated equation simplifications until normal form or fuel exhaustion.
@spec once(Theoria.Env.t(), Theoria.Term.t(), keyword()) :: {:ok, Theoria.Term.t(), Theoria.Simp.Step.t()} | :not_found
Applies one generated equation simplification, if possible.
@spec realize(Theoria.Env.t(), Theoria.Term.t(), keyword()) :: {:ok, Theoria.Equation.Realized.t()} | {:error, term()}
Normalizes and realizes the produced equality as a checked artifact.