mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-09-21 10:18:23 +03:00
Fix formatting
Someone had LaTeX on the brain instead of RST
This commit is contained in:
parent
59800e1f47
commit
7816c6c5e9
@ -64,7 +64,7 @@ and is not required at run-time, as explicitly stated in the types of
|
||||
These use an ``auto``-implicit to pass around
|
||||
a ``State`` with the relevant ``tag`` implicitly, so we refer
|
||||
to states by tag alone. In ``helloCount`` earlier, we used an empty type
|
||||
\texttt{Counter} as the tag:
|
||||
``Counter`` as the tag:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user