Bring back the Bind rule
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?