From 0517d82984234f1a16fba11c7ab2dda6ee09afdb Mon Sep 17 00:00:00 2001 From: Ingo Blechschmidt Date: Fri, 8 Mar 2019 14:01:33 +0100 Subject: [PATCH] [doc] fix markup in two tiny places --- doc/user-manual/language/irrelevance.lagda.rst | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/doc/user-manual/language/irrelevance.lagda.rst b/doc/user-manual/language/irrelevance.lagda.rst index 777d5d87956..68aeab059c1 100644 --- a/doc/user-manual/language/irrelevance.lagda.rst +++ b/doc/user-manual/language/irrelevance.lagda.rst @@ -168,8 +168,7 @@ What can't be done to irrelevant arguments Cannot pattern match against irrelevant argument of type Nat when checking that the pattern zero has type Nat -**Example 4.** We also can't match on an irrelevant record (see - :ref:`record-types`). +**Example 4.** We also can't match on an irrelevant record (see :ref:`record-types`). .. code-block:: agda @@ -225,7 +224,7 @@ Record fields (see :ref:`record-types`) can be marked as irrelevant by prefixing .prop1 : n + m ≡ n * m + 2 .prop2 : suc m ≤ n -**Example 2.** For any type ``A``, we can define a `squashed' version ``Squash A`` where all elements are equal. :: +**Example 2.** For any type ``A``, we can define a 'squashed' version ``Squash A`` where all elements are equal. :: record Squash (A : Set) : Set where constructor squash