Last active
February 26, 2018 23:35
-
-
Save wagle/b3edde1b67f58f63501028b2fa41668e to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
diff --git a/doc/sphinx/addendum/canonical-structures.rst b/doc/sphinx/addendum/canonical-structures.rst | |
index a8975c363..e3594cd26 100644 | |
--- a/doc/sphinx/addendum/canonical-structures.rst | |
+++ b/doc/sphinx/addendum/canonical-structures.rst | |
@@ -200,7 +200,7 @@ over the types that are equipped with both relations. | |
Check forall (e : LE.type) (x y : LE.obj e), x <= y -> y <= x -> x == y. | |
-We need to define a new class that inherits from both ``EQ`` and ``LE`. | |
+We need to define a new class that inherits from both ``EQ`` and ``LE``. | |
.. coqtop:: all | |
@@ -222,7 +222,7 @@ We need to define a new class that inherits from both ``EQ`` and ``LE`. | |
Arguments Class {T} _ _ _. | |
The mixin component of the ``LEQ`` class contains all the extra content we | |
-are adding to ``EQ and ``LE``. In particular it contains the requirement | |
+are adding to ``EQ`` and ``LE``. In particular it contains the requirement | |
that the two relations we are combining are compatible. | |
Unfortunately there is still an obstacle to developing the algebraic | |
@@ -294,7 +294,7 @@ setting to any concrete instate of the algebraic structure. | |
Abort. | |
-Again one has to tell |Coq| that the type ``nat`` is in the ``LEQ` class, and | |
+Again one has to tell |Coq| that the type ``nat`` is in the ``LEQ`` class, and | |
how the type constructor ``*`` interacts with the ``LEQ`` class. In the | |
following proofs are omitted for brevity. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment