Support for capturing substitution about unbound-generics

[TOTBWF]

I totally agree with you on abstracting out the more general notion of substitution out of Subst. As for literature, Erwin Brady's paper on Idris Elaboration should be a good example (especially page 16 and beyond). Other examples would be any other tactic based proof/program refinement systems.

[lambdageek]

@TOTBWF I don't completely follow your example (maybe github isn't the best communication medium - do you have a pointer to a paper with an example language that I can take a look at. Either something from the literature or maybe a draft of something you're working on?)

However, it sounds to me like the notion of substitution that you want for meta-variables is not "plain vanilla capture-avoiding substitution" which is largely what Subst is about.

I do agree that it would be nice if unbound-generics could help with boilerplate of other notions of substitution. So I would propose another path: instead of enriching Subst with new methods, or adding a new sort of variable to the core of unbound-generics, let's look for reusable pieces of Subst that we can abstract out to give us building blocks for writing new substitution algorithms.

Does that make sense?