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