update SET_COMPREHENSION documentation (#8372)
authormudathirmahgoub <mudathirmahgoub@gmail.com>
Wed, 23 Mar 2022 02:53:38 +0000 (21:53 -0500)
committerGitHub <noreply@github.com>
Wed, 23 Mar 2022 02:53:38 +0000 (02:53 +0000)
src/api/cpp/cvc5_kind.h

index c9d10b297487a651b96c6ce33d9b65e726b0f80f..ff170e567f4549cd036c955b9daf8f36c9c0b2e1 100644 (file)
@@ -2208,8 +2208,8 @@ enum Kind : int32_t
    * a predicate P[x1...xn], and a term t[x1...xn]. A comprehension C with the
    * above form has members given by the following semantics:
    * @f[
-   *  \forall y. ( \exists x_1...x_n. P[x_1...x_n] \hat{} t[x_1...x_n] = y )
-   * \Leftrightarrow (member y C)
+   *  \forall y. ( \exists x_1...x_n. P[x_1...x_n] \wedge t[x_1...x_n] = y )
+   * \Leftrightarrow (set.member \; y \; C)
    * @f]
    * where y ranges over the element type of the (set) type of the
    * comprehension. If @f$ t[x_1..x_n] @f$ is not provided, it is equivalent to