At some point I’m gonna want to ask about Tuesday where we added p (prog)/P and all of our in-hole calls had to switch from E to P… I have something missing in my mental model as to why the in-hole switch is necessary… (we

I don’t want to really ask until I have a clear example written up, but I’m not there yet. But if someone wants to preempt my question with an answer I’d be grateful …

We had to change from E to P in in-hole because the notion of what is a program in the language changed. Previously, a program was just an expression. Then, it became the (prog (defun ___) ... e) form. Had we not changed the in-hole, the reduction relation would be unable to find the hole in the e which now lives in the prog form.

@leafac … still trying to understand… but when we wrote the language (iirc), we extended the language adding p but then extended the evaluation context with P… and that had a reference to E. so other than searching for E holes that refer to the defuns (or whatever they were called) in P, why wouldn’t our previous reductions work as-is? (ie, I would think that (if true e_t e_f) -> e_t would match regardless of what evaluation context you were declaring in the in-hole match

I’m also trying to figure out how to do this stuff strictly via the extension functions. I think I can do this if all the reduction rules are named but it still feels wrong (as in, I’m not getting something, not implying that this is broken tooling)

> then extended the evaluation context with P I thought we defined P separately and did not change E