📝 Update tutorial 1 with SymReal

lsrcz · Aug 14, 2024 · d604e37 · d604e37
1 parent 2f7d9a5
commit d604e37
Showing 1 changed file with 5 additions and 3 deletions.
diff --git a/tutorials/1_symbolic_type.ipynb b/tutorials/1_symbolic_type.ipynb
@@ -95,7 +95,8 @@
    "id": "41d7eafe-0e12-4f26-a25c-6bfd5bbdaf9f",
    "metadata": {},
    "source": [
-    "Grisette extends the programming model with symbolic types. In the following code, the [`SymInteger`](https://hackage.haskell.org/package/grisette/docs/Grisette-SymPrim.html#t:SymInteger) represents a symbolic integer, which can be a ***symbolic term*** over ***symbolic constants***.\n",
+    "Grisette extends the programming model with symbolic types and provides a curated, consistent interface for SMT solvers.\n",
+    "In the following code, the [`SymInteger`](https://hackage.haskell.org/package/grisette/docs/Grisette-SymPrim.html#t:SymInteger) represents a symbolic integer, which can be a ***symbolic term*** over ***symbolic constants***.\n",
     "A ***symbolic constant*** is a placeholder for a constant value and can be created using its name with the [`OverloadedStrings`](https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/overloaded_strings.html) extension.\n",
     "\n",
     "Here is an example of the symbolic function that constructs a symbolic term."
@@ -176,10 +177,11 @@
    "metadata": {},
    "source": [
     "Grisette currently provides support for primitive symbolic types for the following types.\n",
-    "You can checkout the documentation for details.\n",
+    "You can check out the documentation for details.\n",
     "\n",
     "- Booleans ([`SymBool`](https://hackage.haskell.org/package/grisette/docs/Grisette-SymPrim.html#t:SymBool)).\n",
     "- Integers ([`SymInteger`](https://hackage.haskell.org/package/grisette/docs/Grisette-SymPrim.html#t:SymInteger)).\n",
+    "- Reals ([`SymReal`](https://hackage.haskell.org/package/grisette/docs/Grisette-SymPrim.html#t:SymReal)).\n",
     "- Symbolic signed ([`SymIntN`](https://hackage.haskell.org/package/grisette/docs/Grisette-SymPrim.html#t:SymIntN)) and unsigned ([`SymWordN`](https://hackage.haskell.org/package/grisette/docs/Grisette-SymPrim.html#t:SymIntN)) bit-vectors.\n",
     "- Arbitrary precision IEEE-754 floating point numbers ([`SymFP`](https://hackage.haskell.org/package/grisette/docs/Grisette-SymPrim.html#t:SymFP)).\n",
     "- Uninterpreted functions ([`=~>`](https://hackage.haskell.org/package/grisette/docs/Grisette-SymPrim.html#t:-61--126--62-), [`-~>`](https://hackage.haskell.org/package/grisette/docs/Grisette-SymPrim.html#t:-45--126--62-))."
@@ -1410,7 +1412,7 @@
    "mimetype": "text/x-haskell",
    "name": "haskell",
    "pygments_lexer": "Haskell",
-   "version": "9.6.5"
+   "version": "9.8.2"
   }
  },
  "nbformat": 4,