AngouriMath

Navigation

← Back to list of members

SubstituteUnderABinder​(AngouriMath.​Entity,​AngouriMath.​Entity,​AngouriMath.​Entity,​AngouriMath.​Entity)

 Method (no overloads)

Summary

body, bound over bound, with x replaced
by value where it occurs free, and the name the binder binds afterwards.

Remarks

Where value holds the bound name, the binder takes a fresh one and keeps
it, as Lambda does: renamed back after the substitution, the value's
occurrence of the name was captured, and integral(t + a, t, 0, 1) with a := t became integral(t + t, t, 0, 1), which is 1 where the integral is t + 1/2.
The body is passed over only where it can change. A body without x, or
under a binder over x itself, is returned as it is; where neither
x nor value holds the bound name, one pass gives what a
renaming would. Renaming it three times at every level, as every binder did, made a chain of
nested integrals cost a multiple of itself per level
(https://github.com/asc-community/AngouriMath/issues/1808).

























Angouri © 2019-2023 · Project's repo · Site's repo · Octicons · Transparency · 4862 pages online