Theoria.Rewrite.Proof.EqRec (theoria v0.6.0)

Copy Markdown View Source

Experimental EqRec-path proof lifting helpers.

The shape may change before 1.0.

Summary

Functions

explain(step)
lift_base(env, result_type, proof, step)
lift_proof(env, result_type, proof, step)

Functions

explain(step)

@spec explain(Theoria.Rewrite.Step.t()) :: Theoria.Rewrite.Proof.Capability.t()

lift_base(env, result_type, proof, step)

@spec lift_base(
  Theoria.Env.t(),
  Theoria.Term.t(),
  Theoria.Term.t(),
  Theoria.Rewrite.Step.t()
) ::
  {:ok, Theoria.Term.t()} | {:error, atom()}

lift_proof(env, result_type, proof, step)

@spec lift_proof(
  Theoria.Env.t(),
  Theoria.Term.t(),
  Theoria.Term.t(),
  Theoria.Rewrite.Step.t()
) ::
  {:ok, Theoria.Term.t()} | {:error, atom()}