Theoria.Rewrite.Proof.Result (theoria v0.5.0)

Experimental proof-diagnostic result for Theoria 0.5 rewrite and simp steps.

The shape may change before 1.0.

Summary

status()

t()

capability(arg1)

checked?(result)

not_requested()

proof(arg1)

status(arg1)

@type status() ::
  :checked
  | :not_requested
  | :missing_rule_proof
  | :unsupported_path
  | :kernel_rejected

@type t() :: %Theoria.Rewrite.Proof.Result{
  capability: Theoria.Rewrite.Proof.Capability.t(),
  proof: Theoria.Term.t() | nil,
  status: status()
}

@spec capability(t() | nil) :: Theoria.Rewrite.Proof.Capability.t() | nil

@spec checked(Theoria.Term.t(), Theoria.Rewrite.Proof.Capability.t()) :: t()

@spec checked?(t() | nil) :: boolean()

@spec not_requested() :: t()

@spec proof(t() | nil) :: Theoria.Term.t() | nil

@spec rejected(status(), Theoria.Rewrite.Proof.Capability.t()) :: t()

@spec status(t() | nil) :: status() | nil