@@ -456,7 +456,7 @@ implicit ``prf`` argument, which has the following type:
457.. code-block:: idris
457.. code-block:: idris
459− prf : InState lbl (State ty) res}
459+ prf : InState lbl (State ty) res
461This relies on a predicate ``InState``. A value of type ``InState x ty res``
461This relies on a predicate ``InState``. A value of type ``InState x ty res``
462means that the reference ``x`` must have type ``ty`` in the list of
462means that the reference ``x`` must have type ``ty`` in the list of