A line of a derivation that a substitution makes from a line before it
The rewrite entity takes the relation of the new line as its optional
first argument, such as ~S"\to_\beta". The default is =. The entity
makes its line from the line before it, or from the line that from names.
replace names the occurrences in the old line: a \part, or a symbol
that within can limit to a part. by names a part of an earlier line,
and a copy of it goes into each place. by_tex gives new LaTeX in place
of by. The option is not with, because with is a special form of
Elixir. to gives a template, and each \use{name} in it is a copy of the
part name. Without replace, the template is the whole new line. drop
names the parts of the old line that the new line does not hold. rule
gives a left side and a right side with the variables of vars, and
Expresso.Element.Math.Rule finds the left side in the old line, or in
the part of replace.
A rewrite takes three steps: :occurrences, :kept and :copies.
steps takes a list of groups, and each group is one step, such as
[[:occurrences, :kept], :copies].
Expresso.Element.Math.check/1 turns each rewrite into an
Expresso.Element.MathLine with Expresso.Element.Math.Rewrite.expand/1.
docs/line-rewrites.md gives the design.
Summary
Types
@type t() :: %Expresso.Element.MathRewrite{ __spark_metadata__: term(), by: term(), by_tex: term(), drop: term(), from: term(), kind: term(), name: term(), paren: term(), relation: term(), replace: term(), rule: term(), steps: term(), to: term(), vars: term(), why: term(), why_tex: term(), within: term() }
The struct of a rewrite of a derivation