search

sweirich / replib

Replib: generic programming & Unbound: generic treatment of binders
MIT License
44 stars 12 forks source link

Variable capture when substituting in patterns #25

Open GoogleCodeExporter opened 9 years ago

GoogleCodeExporter commented 9 years ago 
Should be able to detect & fail when capture occurs while substituting in 
patterns. For example, 

subst (Rebind x y) (Var x)  

will produce an invalid pattern. The variable x will still be a free variable, 
even though the pattern binds variables of that name.  This behavior should be 
caught and an appropriate error message given.

May also be worth having a Maybe version of subst.

Original issue reported on code.google.com by stephanie.weirich on 24 Apr 2013 at 6:56