AngouriMath
MatchableChildren
Property
Summary
The written parts, which is what a pattern has to be able to say. The rename
above is what makes traversal alpha-invariant and it is exactly what puts the
bound name out of a pattern's reach, so matching reads the pair as declared.
#1074
above is what makes traversal alpha-invariant and it is exactly what puts the
bound name out of a pattern's reach, so matching reads the pair as declared.
#1074
Remarks
A pattern that reads these still cannot tell { x : x > 0 } from
{ y : y > 0 } , because the only pattern allowed in the name position
is a hole — MatchPattern's
Binder refuses anything else. It is the hole being repeated in the body
that says "the same variable", and that reads the same under either name.
is a hole — MatchPattern's
that says "the same variable", and that reads the same under either name.
Angouri © 2019-2023 · Project's repo · Site's repo · Octicons · Transparency · 4378 pages online