GitLab

Once #1 (closed) is done: Provide a module ectx_lang for languages with an evaluation context interface, and show that this implies a bind rule. This will be similar to how core_lang looks right now, but not identical - in particular, the user will be in control of fork.

@swasey I recall you changed the core_lang axioms some time ago to actually make some sense. These changed axioms will then become part of ectx_lang. Are they suitably canonical, or is there something we should discuss there? Do we know that an actual Coq implementation of some lambda calculus can satisfy these axioms? Once we have ectx_lang in the development, how much work would it take to port your old AutoSubst-based language to that interface, so that we have a (nice?) example of an instantiated language?