Svtv-idealize-internals
Umbrella topic for internal concepts used in the proofs for the svtv-idealize framework.
Subtopics
- Svtv-override-triplemap-key-check
- Checks that the given key either isn't bound the test alist, or else
has a triple in the triplemap such that the test of the triple is the key's
binding in the test-alist, the val of the triple is the key's binding in the
val-alist, and the refvar of the triple is bound in probes to a probe whose
signal is the key and time is the current phase.