Theoria.Rewrite.Step (theoria v0.4.0)

Copy Markdown View Source

One structural rewrite application with the matched path and optional proof data.

Summary

Types

path_segment()
t()

Types

path_segment()

@type path_segment() :: atom()

t()

@type t() :: %Theoria.Rewrite.Step{
  after: Theoria.Term.t(),
  before: Theoria.Term.t(),
  path: [path_segment()],
  proof: Theoria.Term.t() | nil,
  proof_status:
    :checked
    | :not_requested
    | :missing_rule_proof
    | :unsupported_path
    | :kernel_rejected
    | nil,
  rule: Theoria.Rewrite.Rule.t(),
  substitution: Theoria.Rewrite.Match.substitution() | nil
}