commits
AsyncThunk: add volatile state. This is to be used for thunks that must
always be recomputed.
The code for entering the problem scope in the declaration elaborators
was completely wrong. When entering a field projection scope, we
shouldn't introduce the record but rather just change the cursor!
Previously the environment was "cut off" before the current declaration
to avoid circularity. This was both too conservative (because I wasn't
thinking about the order in which holes get added!) and it was
unnecessary. The right thing to do is simply to only allow an identifier
to be resolved when it refers to a defined term; no cut-off is needed
beyond this.
Adding magic "this" variable name also.
The code for entering the problem scope in the declaration elaborators
was completely wrong. When entering a field projection scope, we
shouldn't introduce the record but rather just change the cursor!
Previously the environment was "cut off" before the current declaration
to avoid circularity. This was both too conservative (because I wasn't
thinking about the order in which holes get added!) and it was
unnecessary. The right thing to do is simply to only allow an identifier
to be resolved when it refers to a defined term; no cut-off is needed
beyond this.