Hiding `spec_ctx`.
In order to make the lower-level "interface" of ReLoC more clear, it could be worth hiding the spec_ctx
predicate;
we can just define new \mapstoS
and \Mapsto
as a conjunction of spec_ctx
and the old mapstoS/Mapsto
.
It might be worth incorporating this into the ext_lp
branch, depending on whether we do something similar there.