Delayed MVar Invocation

Stream: metaprogramming / tactics

[Leni Aniva]

When there is a application node of the form ?m a1 ... an and ?m is delayed assigned (means that it has a list of fvars), is it guaranteed that the length of fvars is not greater than n? If not, from whose context are these fvars instantiated?

[Kyle Miller]

Yes, this is an invariant. I think it's documented inside the code for instantiateMVars. That routine will not instantiate such delayed assignments at all.

[Leni Aniva]

Kyle Miller said:

Yes, this is an invariant. I think it's documented inside the code for instantiateMVars. That routine will not instantiate such delayed assignments at all.

reading the code, it seems like there will not be any delayed assigned mvar nested inside another delayed assigned mvar. Is that true?

[Kyle Miller]

By nested you mean "can delayed assignment mvars be delayed assigned to a delayed assignment"? They can. The code for expanding delayed assignments works by instantiating mvars of the delayed assignment first, and only instantiating if that's got no mvars. If you're looking for some loop to keep instantiating delayed assignments, that's why it's not there.