Theoria.Equality.Chain (theoria v0.5.0)

Builds kernel-checked equality artifacts for rewrite/simp traces.

Summary

step()

t()

new(type, start)

Starts an equality chain at a term of the given type.

Returns the proof term and strategy selected for a chain.

Realizes the chain as a checked equality artifact.

Appends one equality step to the chain.

@type step() :: %{after: Theoria.Term.t(), proof: Theoria.Term.t() | nil}

@type t() :: %Theoria.Equality.Chain{
  current: Theoria.Term.t(),
  start: Theoria.Term.t(),
  steps: [step()],
  type: Theoria.Term.t()
}

@spec new(Theoria.Term.t(), Theoria.Term.t()) :: t()

Starts an equality chain at a term of the given type.

@spec proof_result(t()) :: Theoria.Equality.Chain.Result.t()

Returns the proof term and strategy selected for a chain.

@spec realize(Theoria.Env.t(), t(), Theoria.Equation.Identity.t()) ::
  {:ok, Theoria.Equation.Realized.t()} | {:error, term()}

Realizes the chain as a checked equality artifact.

@spec step(t(), Theoria.Term.t(), Theoria.Term.t() | nil) :: t()

Appends one equality step to the chain.