Theoria.Rewrite.Proof (theoria v0.4.0)

Proof construction helpers for structural rewrite steps.

Summary

Attaches proof status and a checked proof to a rewrite step when possible.

Returns a checked proof for a rewrite step when currently supported.

Instantiates a realized or proof-backed rule proof with the rewrite substitution.

@spec attach(Theoria.Env.t(), Theoria.Rewrite.Step.t()) :: Theoria.Rewrite.Step.t()

Attaches proof status and a checked proof to a rewrite step when possible.

@spec for_step(Theoria.Env.t(), Theoria.Rewrite.Step.t()) :: Theoria.Term.t() | nil

Returns a checked proof for a rewrite step when currently supported.

@spec instantiate_rule(
  Theoria.Rewrite.Rule.t(),
  Theoria.Rewrite.Match.substitution() | nil
) ::
  Theoria.Term.t() | nil

Instantiates a realized or proof-backed rule proof with the rewrite substitution.