diff options
| -rw-r--r-- | doc/sphinx/addendum/ring.rst | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst index 20e4c6a3d6..3b350d5dc0 100644 --- a/doc/sphinx/addendum/ring.rst +++ b/doc/sphinx/addendum/ring.rst @@ -323,7 +323,7 @@ The syntax for adding a new ring is decidable :n:`@term` declares the ring as computational. The expression :n:`@term` is the correctness proof of an equality test ``?=!`` - (which hould be evaluable). Its type should be of the form + (which should be evaluable). Its type should be of the form ``forall x y, x ?=! y = true → x == y``. morphism :n:`@term` |