From: mudathirmahgoub <mudathirmahgoub@gmail.com>
Date: Wed, 23 Mar 2022 02:53:38 +0000 (-0500)
Subject: update SET_COMPREHENSION documentation (#8372)
X-Git-Tag: cvc5-1.0.0~201
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7e0866c1c05d06d77c783575d991f75a2da9b59c;p=cvc5.git

update SET_COMPREHENSION documentation (#8372)
---

diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h
index c9d10b297..ff170e567 100644
--- a/src/api/cpp/cvc5_kind.h
+++ b/src/api/cpp/cvc5_kind.h
@@ -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