You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Unbound/RepLib had these additional binders that allow you to express patterns where the bound names are treated in such a way that their order doesn't matter. (For example you could create a term local x=1, y=2 in e((x,y)) which is alpha-equivalent to local y=2, x=1 in e.)
It should be pretty straightforward to add this back in. All the magic is in the smart constructors setbind and setplusbind. (One would also need to generalize Bind to GenBind as in Unbound. No big deal)
The text was updated successfully, but these errors were encountered:
Unbound/RepLib had these additional binders that allow you to express patterns where the bound names are treated in such a way that their order doesn't matter. (For example you could create a term
local x=1, y=2 in e((x,y))
which is alpha-equivalent tolocal y=2, x=1 in e
.)It should be pretty straightforward to add this back in. All the magic is in the smart constructors
setbind
andsetplusbind
. (One would also need to generalizeBind
toGenBind
as in Unbound. No big deal)The text was updated successfully, but these errors were encountered: