Ideally, #%top-interaction should be wrapped in with-vc to reset the VC in case of a Rosette error that sets the VC as a contradiction. However, this isn't so easy because we want the top-level to support definitions and with-vc creates a definition context. Sadly, there is no splicing form of with-vc right now. We will need to hack something up custom.
Ideally,
#%top-interactionshould be wrapped inwith-vcto reset the VC in case of a Rosette error that sets the VC as a contradiction. However, this isn't so easy because we want the top-level to support definitions andwith-vccreates a definition context. Sadly, there is no splicing form ofwith-vcright now. We will need to hack something up custom.