Revise the guide: Reflecting on Symbolic State.

sorawee · Feb 13, 2021 · d34c2ae · d34c2ae
1 parent 091b669
commit d34c2ae
Showing 1 changed file with 6 additions and 2 deletions.
diff --git a/rosette/guide/scribble/reflection/state-reflection.scrbl b/rosette/guide/scribble/reflection/state-reflection.scrbl
@@ -105,8 +105,7 @@ best to use them sparingly.
 }
 
 
-@deftogether[(@defproc[(vc) vc?]
-              @defproc[(clear-vc!) void?])]{
+@defproc[(vc) vc?]{
 
  The current @tech{verification condition}, @racket[(vc)],
  is a value of type @racket[vc?]. At the start of evaluation,
@@ -132,6 +131,11 @@ best to use them sparingly.
 (vc)]
 }
 
+@defproc[(clear-vc!) void?]{
+Clears the current verification condition by setting it to @racket[vc-true].
+See @racket[vc] for details.               
+}
+
 @defform*[((with-vc expr)
            (with-vc vc-expr expr))
           #:contracts ([vc-expr vc?])]{