Missing substitution rule in exercise “let rec”

[cionx]

In the exercise “let rec”, we add the new language construct rec to OCaml Core. But the exercise seems to forget to explain how substitution works for this new construct, i.e., how the following term is defined:

(rec f -> e){v/x}

But we need this kind of substitution to solve the exercise, as can also be seen in the official solutions: to derive a used equality, we need to know what F{3/x} is, where F is an expression of the form rec fact -> ...

From what I understand, this missing substitution rule should be as follows:

(rec f -> e){v/x} = rec f -> e{v/x}   if x <> f
(rec f -> e){v/f} = rec f -> e

[clarksmr]

Thank you!

Since rec is a binder, I suspect we need to be careful about capturing-avoiding substitution here, too. That means another side condition:

(rec f -> e){v/x} = rec f -> e{v/x}   if x <> f, and f not in FV(v)
(rec f -> e){v/f} = rec f -> e

This is how the fun binding is handled, too:

https://github.com/cs3110/textbook/blob/dcc2f40d773c651aaca08fb789bf06f4eb645b95/src/chapters/interp/substitution.md?plain=1#L1005-L1008

I haven't found this in any of my usual sources though (e.g., TAPL). Would be nice to double-check — it's much too easy to get capture-avoiding substitution wrong!

I'll go ahead and push those rules anyway. If you discover a further improvement, please reopen.