From 774770af22c882ade8f44aedbeed027cdf3d9496 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Fri, 3 Dec 2021 11:07:46 -0800 Subject: [PATCH] Fix a few broken links (#7734) This PR fixes a few broken links in our documentation. --- docs/api/python/regular/quickstart.rst | 2 +- docs/theories/separation-logic.rst | 2 +- docs/theories/sets-and-relations.rst | 3 ++- 3 files changed, 4 insertions(+), 3 deletions(-) diff --git a/docs/api/python/regular/quickstart.rst b/docs/api/python/regular/quickstart.rst index 783bcfd1f..ba3360db8 100644 --- a/docs/api/python/regular/quickstart.rst +++ b/docs/api/python/regular/quickstart.rst @@ -166,7 +166,7 @@ Example ------- | The SMT-LIB input for this example can be found at `examples/api/smtlib/quickstart.smt2 `_. -| The source code for this example can be found at `examples/api/python/quickstart.py `_. +| The source code for this example can be found at `examples/api/python/quickstart.py `_. .. api-examples:: /api/cpp/quickstart.cpp diff --git a/docs/theories/separation-logic.rst b/docs/theories/separation-logic.rst index 86f802ef8..36d3a165f 100644 --- a/docs/theories/separation-logic.rst +++ b/docs/theories/separation-logic.rst @@ -121,7 +121,7 @@ formula ``(not (emp x 0))`` is satisfied by heaps ``U -> Int`` (the sorts of (check-sat) The following input on heaps ``Int -> Node`` is satisfiable, where ``Node`` -denotes a user-defined inductive `datatypes `__. +denotes a user-defined inductive :doc:`datatypes`. .. code:: smtlib diff --git a/docs/theories/sets-and-relations.rst b/docs/theories/sets-and-relations.rst index 2da6715e3..bed7e05cf 100644 --- a/docs/theories/sets-and-relations.rst +++ b/docs/theories/sets-and-relations.rst @@ -16,7 +16,8 @@ The source code of these examples is available at: * `SMT-LIB 2 language example `__ * `C++ API example `__ -* `Python API example `__ +* `Java API example `__ +* `Python API example `__ Below is a short summary of the sorts, constants, functions and -- 2.30.2