Capture avoidance in substitution

[Blaisorblade]

How do you prevent variable capture in substitution?

I think your code would cause capture with (for instance) subst("fun x -> y", "y", "x z") (where I write concrete syntax instead of ASTs). That could be triggered when normalizing (fun y -> fun x -> y) (x z). With your current code, this example won't be a problem since you have an evaluator, which refuses open terms; so I'm not sure this bug can already be triggered in this particular way.

But (I'd say) this is the sort of thing that at the very least deserves a comment. Alternatively, I'd just implement (some variant of) capture-avoiding substitution.

See the intro to chapter 6 of Pierce's TAPL for a list of approaches.