diff --git a/src/sphinx/verification.rst b/src/sphinx/verification.rst index eed3450933411c847f3d6a053b7bf112bd3be25e..b8af549751c717d48f1b3d4af43a422ef109d26b 100644 --- a/src/sphinx/verification.rst +++ b/src/sphinx/verification.rst @@ -57,7 +57,7 @@ the following for any number of parameters): } ensuring(r => post) where, :math:`\mbox{prec}(x)` is a Boolean expression with free variables -contained in :math:`\{ x \}`, :math:`\mbox{body}(x)` is a Boolean expression with +contained in :math:`\{ x \}`, :math:`\mbox{body}(x)` is an expression with free variables contained in :math:`\{ x \}` and :math:`\mbox{post}(x, r)` is a Boolean expression with free variables contained in :math:`\{ x, r \}`. The types of :math:`x` and :math:`r` are respectively ``A`` and ``B``. We write