track has_lc directly in invGS/irisGS/heapGS rather than via separate typeclass
When I tried to make heapGS
be credit-enabled by default (!809 (closed)), I realized the current scheme of using a HasLc
typeclass does not work as well as we had hoped.
So here's an alternative that @robbertkrebbers and me came up with: add a has_lc
parameter to invGS
/irisGS
/heapGS
that tracks whether this instance of the logic has later credits or not. The existing short names invGS
/irisGS
/heapGS
refer to having credits; new invGS_gen
/etc can be sued to be generic over whether credits are present or to state the absence of credits (for some juicy fupd-plainly-rules).
This seems to work as intended, all the HeapLang examples now implicitly have credits available. (Not that they can do much with that, but one day... ;) @lgaeher @simonspies what do you think?