idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-29 14:44:03 +03:00
Code Issues Projects Releases Wiki Activity

Remove the :force: that RTD complains about

Browse Source 
This isn't the right solution since it removes the highlighting but
maybe it makes the build work again (it does for me locally)
This commit is contained in:
Edwin Brady 2020-05-20 18:46:09 +01:00
parent 0563f7dcec
commit 940570e083
2 changed files with 2 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
docs/source/tutorial/miscellany.rst
View File

@ -93,15 +93,12 @@ only. Usually, ``default`` is used to provide things like a custom proof search
Literate programming
====================
[NOT YET IN IDRIS 2]
Like Haskell, Idris supports *literate* programming. If a file has
an extension of ``.lidr`` then it is assumed to be a literate file. In
literate programs, everything is assumed to be a comment unless the line
begins with a greater than sign ``>``, for example:
.. code-block:: literate-idris
:force:
::
> module literate

3
docs/source/tutorial/modules.rst
View File

@ -147,8 +147,7 @@ Propagating Inner Module API's
Additionally, a module can re-export a module it has imported, by using
the ``public`` modifier on an ``import``. For example:
.. code-block:: idris
:force:
::
module A