From aef165673abe2e5a3da0a056fe5994249629140f Mon Sep 17 00:00:00 2001
From: ptrcarta <ptrcarta@gmail.com>
Date: Tue, 31 May 2016 12:57:50 +0200
Subject: [PATCH] documetation bug about the type of body expression
`body` doesn't need to be a Boolean expression
---
src/sphinx/verification.rst | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/sphinx/verification.rst b/src/sphinx/verification.rst
index eed345093..b8af54975 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
--
GitLab