fix sphinx warnings

disco-lang · Dec 22, 2024 · 78ad2ea · 78ad2ea
1 parent a021cbd
commit 78ad2ea
Show file tree

Hide file tree

Showing 18 changed files with 30 additions and 30 deletions.
diff --git a/docs/introduction/files.rst b/docs/introduction/files.rst
diff --git a/docs/reference/addition.rst b/docs/reference/addition.rst
@@ -4,8 +4,8 @@ Addition
 .. note::
 
    This page concerns the ``+`` operator on numbers; for the ``+``
-   operator on :doc:`types <types>`, see :doc:`sum types <sumtype>`;
-   or see the ``+`` (``overlay``) operator on :doc:`graphs <graphs>`.
+   operator on :doc:`types <types>`, see :doc:`sum types <sum-type>`;
+   or see the ``+`` (``overlay``) operator on :doc:`graphs <graph>`.
 
 Values of all :doc:`numeric types <numeric>` can be added using the ``+``
 operator.  For example:
@@ -25,6 +25,6 @@ If you ask for the :doc:`type <types>` of ``+``, you get
     ~+~ : ℕ × ℕ → ℕ
 
 which says that it is a :doc:`function <function>` taking :doc:`a pair
-of <product>` natural numbers and returning a natural number.
+of <product-type>` natural numbers and returning a natural number.
 However, as mentioned above, it also works on other numeric types such
 as integers and rational numbers.
diff --git a/docs/reference/collection-ops.rst b/docs/reference/collection-ops.rst
@@ -1,5 +1,5 @@
 Collection operations
-====================
+=====================
 
 The :doc:`Cartesian product <cp>` of two collections (:doc:`finite sets
 <set>`, :doc:`lists <list>`, or :doc:`bags <bag>`) can be found

diff --git a/docs/reference/compare.rst b/docs/reference/compare.rst
@@ -20,7 +20,7 @@ can be compared:
 See the individual pages about each type for more information on how
 comparison works on values of that type.
 
-:doc:`Functions <function-type>`, on the other hand, cannot be
+:doc:`Functions <function-types>`, on the other hand, cannot be
 compared, because in general this would require testing the functions
 on every single possible input, of which there might be infinitely
 many.

diff --git a/docs/reference/multiplication.rst b/docs/reference/multiplication.rst
@@ -5,7 +5,7 @@ Multiplication
 
    This page concerns the ``*`` operator on numbers; for the ``*``
    operator on :doc:`types <types>`, see :doc:`pair types
-   <product-type>`; or see the ``*`` (``connect``) operator on :doc:`graphs <graphs>`.
+   <product-type>`; or see the ``*`` (``connect``) operator on :doc:`graphs <graph>`.
 
 All :doc:`numeric types <numeric>` can be multiplied using the ``*``
 operator.  For example:

diff --git a/docs/reference/natural.rst b/docs/reference/natural.rst
@@ -17,7 +17,7 @@ counting numbers 0, 1, 2, 3, 4, 5, ...
    6 : ℕ
 
 Natural numbers cannot be directly :doc:`subtracted <subtraction>` or
-:doc:`divided <division>`.  However, ``N`` is a :doc:`subtype` of all
+:doc:`divided <division>`.  However, ``N`` is a :doc:`subtypes` of all
 the other numeric types, so using subtraction or division with natural
 numbers will cause them to be automatically converted into a
 different type like :doc:`integers <integer>` or :doc:`rationals

diff --git a/docs/reference/no-search.rst b/docs/reference/no-search.rst
@@ -1,7 +1,7 @@
 The type T is not searchable
 ============================
 
-When writing a :doc:`property <property>` using a ``forall``, we are
+When writing a :doc:`property <prop>` using a ``forall``, we are
 only allowed to use types which are *searchable*, that is, types for
 which we can effectively generate sample values.  Note this is not the
 same thing as being finite.  For example, the type of natural numbers

diff --git a/docs/reference/not-qual.rst b/docs/reference/not-qual.rst
@@ -8,4 +8,4 @@ operations to types that do not allow that operation.  For example:
   two :doc:`natural numbers <natural>`
 
 - Trying to :doc:`compare <compare>` two :doc:`functions
-  <function-type>`
+  <function-types>`
diff --git a/docs/reference/numeric.rst b/docs/reference/numeric.rst
@@ -53,7 +53,7 @@ We can arrange the four numeric types in a diamond shape, like this:
    :alt: Diamond lattice
    :align: center
 
-Each type is a subset, or :doc:`subtype`, of the type or types above
+Each type is a subset, or :doc:`subtypes`, of the type or types above
 it.  For example, the fact that :math:`\mathbb{N}` is below
 :math:`\mathbb{Z}` means that every natural number is also an integer.
 

diff --git a/docs/reference/operator.rst b/docs/reference/operator.rst
@@ -8,8 +8,8 @@ their two arguments, like ``1 + 2``.  Disco has many built-in
 operators which are symbols (like ``+``, ``*``, ``/``, *etc.*) as well
 as a few which are words (like ``mod``, ``choose``, and ``divides``).
 
-Disco also has three *unary* operators: :doc:`arithmetic negation <neg>` (``-``)
-and :doc:`logical negation <not>` (``¬`` or ``not``) are written in front of their
+Disco also has three *unary* operators: :doc:`arithmetic negation <subtraction>` (``-``)
+and :doc:`logical negation <logic-ops>` (``¬`` or ``not``) are written in front of their
 one argument, and :doc:`factorial <factorial>` (``!``) is written after its argument.
 
 When multiple operators are used together, Disco uses their
@@ -38,7 +38,7 @@ Note that in this case, we can write ``!`` or ``~!`` and Disco
 understands either one.
 
 The twiddle notation is also useful when giving an operator as an
-argument to a :doc:`higher-order function <hof>`:
+argument to a :doc:`higher-order function <higher-order>`:
 
 ::
 

diff --git a/docs/reference/pattern-type.rst b/docs/reference/pattern-type.rst
@@ -3,7 +3,7 @@ The pattern p is supposed to have type T, but instead...
 
 This is a similar sort of error as :doc:`notcon`, but concerns
 :doc:`patterns <pattern>` instead of :doc:`expressions <expression>`.
-On the one hand, disco can figure out what :doc:`type <type>` a
+On the one hand, disco can figure out what :doc:`type <types>` a
 pattern should be based on the type of the :doc:`function <function>`.
 On the other hand, the pattern itself may correspond to a different
 type.  For example,

diff --git a/docs/reference/prop.rst b/docs/reference/prop.rst
@@ -12,8 +12,8 @@ Any :doc:`Boolean <bool>` expression can be used as a proposition.
 For example, ``T``, ``x > 5``, and ``(x < y) -> ((x == 2) \/ (x ==
 3))`` can all be used as propositions.
 
-However, unlike Boolean expressions, propositions can use :doc:`quantifiers
-<quantifier>`, that is, ``forall`` or ``exists``.  For example,
+However, unlike Boolean expressions, propositions can use
+*quantifiers*, that is, ``forall`` or ``exists``.  For example,
 ``forall x : Z. x^2 >= 0`` is a ``Prop`` (but not a ``Bool``).
 
 If you type a proposition at the Disco prompt, it will simply print
@@ -23,12 +23,14 @@ whether a proposition is true or false, you have two options:
 - The built-in ``holds`` function tries its best to determine whether
   a proposition is true or false.  If it returns a value at all, it is
   definitely correct.  For example,
-    - ``holds ((5 < 3) \/ ((2 < 1) -> F))`` yields ``T``
-    - ``holds (forall p:Bool. forall q:Bool. (p \/ q) <-> (q \/ p))``
-      yields ``T``
-    - ``holds (forall p:Bool. forall q:Bool. (p \/ q) <-> (p /\ q))``
-      yields ``F``
-    - ``holds (forall n:N. n < 529)`` yields ``F``
+
+  - ``holds ((5 < 3) \/ ((2 < 1) -> F))`` yields ``T``
+  - ``holds (forall p:Bool. forall q:Bool. (p \/ q) <-> (q \/ p))``
+    yields ``T``
+  - ``holds (forall p:Bool. forall q:Bool. (p \/ q) <-> (p /\ q))``
+    yields ``F``
+  - ``holds (forall n:N. n < 529)`` yields ``F``
+
   However, sometimes it may simply get stuck in an infinite loop.  For
   example, ``holds (forall n:N. n >= 0)`` will simply get stuck. Even
   though it is obvious to us that this proposition is true, ``holds``
@@ -41,6 +43,7 @@ whether a proposition is true or false, you have two options:
   output much more information than a simple ``T`` or ``F``,
   for example, showing a counterexample if a ``forall`` is false, or a
   witness if an ``exists`` is true.  For example,
+
     - ``:test forall p:Bool. forall q:Bool. (p \/ q) <-> (p /\ q)``
       prints
 

diff --git a/docs/reference/size.rst b/docs/reference/size.rst
@@ -1,7 +1,7 @@
 Size
 ====
 
-The *size* of a :doc:`collection <collection-types>` ``c`` (a :doc:`list
+The *size* of a :doc:`collection <collections>` ``c`` (a :doc:`list
 <list>`, :doc:`bag <bag>`, or :doc:`set <set>`) can be found using the
 notation ``|c|``.  For example,
 

diff --git a/docs/reference/sum-type.rst b/docs/reference/sum-type.rst
@@ -23,7 +23,7 @@ Sum types
 
 Note that the ``left`` or ``right`` ensures that ``A + B`` really does
 represent a *disjoint* union.  For example, although the usual
-:doc:`union <union>` operator is idempotent, that is,
+:doc:`union <collection-ops>` operator is idempotent, that is,
 :math:`\mathbb{N} \cup \mathbb{N} = \mathbb{N}`, with a disjoint union
 of types ``N + N`` is not at all the same as ``N``.  Elements of ``N +
 N`` look like either ``left(3)`` or ``right(3)``, that is, ``N + N``

diff --git a/docs/reference/types.rst b/docs/reference/types.rst
@@ -33,10 +33,9 @@ is a :doc:`subtype <subtypes>` of the one it was expecting.
    type-sig
    type-annot
    polymorphism
-   type-annot
    algebraic-types
    typedef
-   collection-types
+   collections
    string
    prop
    subtypes
diff --git a/docs/reference/variable.rst b/docs/reference/variable.rst
@@ -8,7 +8,7 @@ a letter.  For example, ``myHorse3``, ``some_name``, and ``X__17'x'_``
 are all valid variable names.
 
 To define a variable, one must first use a :doc:`type signature
-<type-sig>` to declare its :doc:`type` on a line by itself, like
+<type-sig>` to declare its :doc:`type <types>` on a line by itself, like
 
 ::
 

diff --git a/docs/requirements.txt b/docs/requirements.txt
@@ -1,3 +1,3 @@
-sphinx==8.1.3
+sphinx==7.2.6
 sphinx-rtd-theme==3.0.2
 sphinx-notfound-page==1.0.4
diff --git a/docs/tutorial/typedefs.rst b/docs/tutorial/typedefs.rst
@@ -70,7 +70,6 @@ Type definitions can also be parameterized. For example, we can make
 the ``Tree`` type polymorphic:
 
 .. literalinclude:: example/tydefs-poly.disco
-   :language: idris
    :caption:
 
 ::