mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-11-23 20:22:34 +03:00
Merge branch 'jeetu7-master'
This commit is contained in:
Edwin Brady
commit
69e774bd00
2
.gitignore
vendored
2
.gitignore
vendored
@ -10,7 +10,7 @@
|
||||
|
||||
/dist/idris2.c
|
||||
|
||||
/docs/_build/
|
||||
/docs/build/
|
||||
|
||||
/libs/**/build
|
||||
/tests/**/output
|
||||
|
||||
191
docs/Makefile
191
docs/Makefile
@ -1,183 +1,20 @@
|
||||
# Makefile for Sphinx documentation
|
||||
# Minimal makefile for Sphinx documentation
|
||||
#
|
||||
|
||||
# You can set these variables from the command line.
|
||||
SPHINXOPTS =
|
||||
SPHINXBUILD = sphinx-build
|
||||
PAPER =
|
||||
BUILDDIR = _build
|
||||
|
||||
# User-friendly check for sphinx-build
|
||||
ifeq ($(shell which $(SPHINXBUILD) >/dev/null 2>&1; echo $$?), 1)
|
||||
$(error The '$(SPHINXBUILD)' command was not found. Make sure you have Sphinx installed, then set the SPHINXBUILD environment variable to point to the full path of the '$(SPHINXBUILD)' executable. Alternatively you can add the directory with the executable to your PATH. If you don't have Sphinx installed, grab it from https://www.sphinx-doc.org/)
|
||||
endif
|
||||
|
||||
# Internal variables.
|
||||
PAPEROPT_a4 = -D latex_paper_size=a4
|
||||
PAPEROPT_letter = -D latex_paper_size=letter
|
||||
ALLSPHINXOPTS = -d $(BUILDDIR)/doctrees $(PAPEROPT_$(PAPER)) $(SPHINXOPTS) .
|
||||
# the i18n builder cannot share the environment and doctrees with the others
|
||||
I18NSPHINXOPTS = $(PAPEROPT_$(PAPER)) $(SPHINXOPTS) .
|
||||
|
||||
.PHONY: help clean html dirhtml singlehtml pickle json htmlhelp qthelp devhelp epub latex latexpdf text man changes linkcheck doctest coverage gettext
|
||||
# You can set these variables from the command line, and also
|
||||
# from the environment for the first two.
|
||||
SPHINXOPTS ?=
|
||||
SPHINXBUILD ?= sphinx-build
|
||||
SOURCEDIR = source
|
||||
BUILDDIR = build
|
||||
|
||||
# Put it first so that "make" without argument is like "make help".
|
||||
help:
|
||||
@echo "Please use \`make <target>' where <target> is one of"
|
||||
@echo " html to make standalone HTML files"
|
||||
@echo " dirhtml to make HTML files named index.html in directories"
|
||||
@echo " singlehtml to make a single large HTML file"
|
||||
@echo " pickle to make pickle files"
|
||||
@echo " json to make JSON files"
|
||||
@echo " htmlhelp to make HTML files and a HTML help project"
|
||||
@echo " qthelp to make HTML files and a qthelp project"
|
||||
@echo " devhelp to make HTML files and a Devhelp project"
|
||||
@echo " epub to make an epub"
|
||||
@echo " latex to make LaTeX files, you can set PAPER=a4 or PAPER=letter"
|
||||
@echo " latexpdf to make LaTeX files and run them through pdflatex"
|
||||
@echo " latexpdfja to make LaTeX files and run them through platex/dvipdfmx"
|
||||
@echo " text to make text files"
|
||||
@echo " man to make manual pages"
|
||||
@echo " texinfo to make Texinfo files"
|
||||
@echo " info to make Texinfo files and run them through makeinfo"
|
||||
@echo " gettext to make PO message catalogs"
|
||||
@echo " changes to make an overview of all changed/added/deprecated items"
|
||||
@echo " xml to make Docutils-native XML files"
|
||||
@echo " pseudoxml to make pseudoxml-XML files for display purposes"
|
||||
@echo " linkcheck to check all external links for integrity"
|
||||
@echo " doctest to run all doctests embedded in the documentation (if enabled)"
|
||||
@echo " coverage to run coverage check of the documentation (if enabled)"
|
||||
@$(SPHINXBUILD) -M help "$(SOURCEDIR)" "$(BUILDDIR)" $(SPHINXOPTS) $(O)
|
||||
|
||||
clean:
|
||||
rm -rf $(BUILDDIR)/*
|
||||
.PHONY: help Makefile
|
||||
|
||||
html:
|
||||
$(SPHINXBUILD) -b html $(ALLSPHINXOPTS) $(BUILDDIR)/html
|
||||
@echo
|
||||
@echo "Build finished. The HTML pages are in $(BUILDDIR)/html."
|
||||
|
||||
dirhtml:
|
||||
$(SPHINXBUILD) -b dirhtml $(ALLSPHINXOPTS) $(BUILDDIR)/dirhtml
|
||||
@echo
|
||||
@echo "Build finished. The HTML pages are in $(BUILDDIR)/dirhtml."
|
||||
|
||||
singlehtml:
|
||||
$(SPHINXBUILD) -b singlehtml $(ALLSPHINXOPTS) $(BUILDDIR)/singlehtml
|
||||
@echo
|
||||
@echo "Build finished. The HTML page is in $(BUILDDIR)/singlehtml."
|
||||
|
||||
pickle:
|
||||
$(SPHINXBUILD) -b pickle $(ALLSPHINXOPTS) $(BUILDDIR)/pickle
|
||||
@echo
|
||||
@echo "Build finished; now you can process the pickle files."
|
||||
|
||||
json:
|
||||
$(SPHINXBUILD) -b json $(ALLSPHINXOPTS) $(BUILDDIR)/json
|
||||
@echo
|
||||
@echo "Build finished; now you can process the JSON files."
|
||||
|
||||
htmlhelp:
|
||||
$(SPHINXBUILD) -b htmlhelp $(ALLSPHINXOPTS) $(BUILDDIR)/htmlhelp
|
||||
@echo
|
||||
@echo "Build finished; now you can run HTML Help Workshop with the" \
|
||||
".hhp project file in $(BUILDDIR)/htmlhelp."
|
||||
|
||||
qthelp:
|
||||
$(SPHINXBUILD) -b qthelp $(ALLSPHINXOPTS) $(BUILDDIR)/qthelp
|
||||
@echo
|
||||
@echo "Build finished; now you can run "qcollectiongenerator" with the" \
|
||||
".qhcp project file in $(BUILDDIR)/qthelp, like this:"
|
||||
@echo "# qcollectiongenerator $(BUILDDIR)/qthelp/IdrisManual.qhcp"
|
||||
@echo "To view the help file:"
|
||||
@echo "# assistant -collectionFile $(BUILDDIR)/qthelp/IdrisManual.qhc"
|
||||
|
||||
devhelp:
|
||||
$(SPHINXBUILD) -b devhelp $(ALLSPHINXOPTS) $(BUILDDIR)/devhelp
|
||||
@echo
|
||||
@echo "Build finished."
|
||||
@echo "To view the help file:"
|
||||
@echo "# mkdir -p $$HOME/.local/share/devhelp/IdrisManual"
|
||||
@echo "# ln -s $(BUILDDIR)/devhelp $$HOME/.local/share/devhelp/IdrisManual"
|
||||
@echo "# devhelp"
|
||||
|
||||
epub:
|
||||
$(SPHINXBUILD) -b epub $(ALLSPHINXOPTS) $(BUILDDIR)/epub
|
||||
@echo
|
||||
@echo "Build finished. The epub file is in $(BUILDDIR)/epub."
|
||||
|
||||
latex:
|
||||
$(SPHINXBUILD) -b latex $(ALLSPHINXOPTS) $(BUILDDIR)/latex
|
||||
@echo
|
||||
@echo "Build finished; the LaTeX files are in $(BUILDDIR)/latex."
|
||||
@echo "Run \`make' in that directory to run these through (pdf)latex" \
|
||||
"(use \`make latexpdf' here to do that automatically)."
|
||||
|
||||
latexpdf:
|
||||
$(SPHINXBUILD) -b latex $(ALLSPHINXOPTS) $(BUILDDIR)/latex
|
||||
@echo "Running LaTeX files through pdflatex..."
|
||||
$(MAKE) -C $(BUILDDIR)/latex all-pdf
|
||||
@echo "pdflatex finished; the PDF files are in $(BUILDDIR)/latex."
|
||||
|
||||
latexpdfja:
|
||||
$(SPHINXBUILD) -b latex $(ALLSPHINXOPTS) $(BUILDDIR)/latex
|
||||
@echo "Running LaTeX files through platex and dvipdfmx..."
|
||||
$(MAKE) -C $(BUILDDIR)/latex all-pdf-ja
|
||||
@echo "pdflatex finished; the PDF files are in $(BUILDDIR)/latex."
|
||||
|
||||
text:
|
||||
$(SPHINXBUILD) -b text $(ALLSPHINXOPTS) $(BUILDDIR)/text
|
||||
@echo
|
||||
@echo "Build finished. The text files are in $(BUILDDIR)/text."
|
||||
|
||||
man:
|
||||
$(SPHINXBUILD) -b man $(ALLSPHINXOPTS) $(BUILDDIR)/man
|
||||
@echo
|
||||
@echo "Build finished. The manual pages are in $(BUILDDIR)/man."
|
||||
|
||||
texinfo:
|
||||
$(SPHINXBUILD) -b texinfo $(ALLSPHINXOPTS) $(BUILDDIR)/texinfo
|
||||
@echo
|
||||
@echo "Build finished. The Texinfo files are in $(BUILDDIR)/texinfo."
|
||||
@echo "Run \`make' in that directory to run these through makeinfo" \
|
||||
"(use \`make info' here to do that automatically)."
|
||||
|
||||
info:
|
||||
$(SPHINXBUILD) -b texinfo $(ALLSPHINXOPTS) $(BUILDDIR)/texinfo
|
||||
@echo "Running Texinfo files through makeinfo..."
|
||||
make -C $(BUILDDIR)/texinfo info
|
||||
@echo "makeinfo finished; the Info files are in $(BUILDDIR)/texinfo."
|
||||
|
||||
gettext:
|
||||
$(SPHINXBUILD) -b gettext $(I18NSPHINXOPTS) $(BUILDDIR)/locale
|
||||
@echo
|
||||
@echo "Build finished. The message catalogs are in $(BUILDDIR)/locale."
|
||||
|
||||
changes:
|
||||
$(SPHINXBUILD) -b changes $(ALLSPHINXOPTS) $(BUILDDIR)/changes
|
||||
@echo
|
||||
@echo "The overview file is in $(BUILDDIR)/changes."
|
||||
|
||||
linkcheck:
|
||||
$(SPHINXBUILD) -b linkcheck $(ALLSPHINXOPTS) $(BUILDDIR)/linkcheck
|
||||
@echo
|
||||
@echo "Link check complete; look for any errors in the above output " \
|
||||
"or in $(BUILDDIR)/linkcheck/output.txt."
|
||||
|
||||
doctest:
|
||||
$(SPHINXBUILD) -b doctest $(ALLSPHINXOPTS) $(BUILDDIR)/doctest
|
||||
@echo "Testing of doctests in the sources finished, look at the " \
|
||||
"results in $(BUILDDIR)/doctest/output.txt."
|
||||
|
||||
coverage:
|
||||
$(SPHINXBUILD) -b coverage $(ALLSPHINXOPTS) $(BUILDDIR)/coverage
|
||||
@echo "Testing of coverage in the sources finished, look at the " \
|
||||
"results in $(BUILDDIR)/coverage/python.txt."
|
||||
|
||||
xml:
|
||||
$(SPHINXBUILD) -b xml $(ALLSPHINXOPTS) $(BUILDDIR)/xml
|
||||
@echo
|
||||
@echo "Build finished. The XML files are in $(BUILDDIR)/xml."
|
||||
|
||||
pseudoxml:
|
||||
$(SPHINXBUILD) -b pseudoxml $(ALLSPHINXOPTS) $(BUILDDIR)/pseudoxml
|
||||
@echo
|
||||
@echo "Build finished. The pseudo-XML files are in $(BUILDDIR)/pseudoxml."
|
||||
# Catch-all target: route all unknown targets to Sphinx using the new
|
||||
# "make mode" option. $(O) is meant as a shortcut for $(SPHINXOPTS).
|
||||
%: Makefile
|
||||
@$(SPHINXBUILD) -M $@ "$(SOURCEDIR)" "$(BUILDDIR)" $(SPHINXOPTS) $(O)
|
||||
|
||||
@ -11,6 +11,7 @@ To build the manual the following dependencies must be met. We assume that you h
|
||||
|
||||
Python should be installed by default on most systems.
|
||||
Sphinx can be installed either through your hosts package manager or using pip/easy_install.
|
||||
Recommended way is to use virtual environment for building documentation.
|
||||
|
||||
*Note* [ReadTheDocs](https://readthedocs.org) works with Sphinx
|
||||
`v1.2.2`. If you install a more recent version of sphinx then
|
||||
@ -18,9 +19,12 @@ Sphinx can be installed either through your hosts package manager or using pip/e
|
||||
of readthedocs and be ignored. In the past we had several code-blocks
|
||||
disappear because of that.
|
||||
|
||||
The ReadTheDocs theme can be installed using pip as follows:
|
||||
The ReadTheDocs theme can be installed in virtual environment using pip as follows:
|
||||
|
||||
```sh
|
||||
python3 -m venv idris2docs_venv
|
||||
source idris2docs_venv/bin/activate
|
||||
pip install --upgrade pip
|
||||
pip install sphinx_rtd_theme
|
||||
```
|
||||
|
||||
@ -32,6 +36,7 @@ LaTeX can be install either using your systems package manager or direct from Te
|
||||
## Build Instructions
|
||||
|
||||
```sh
|
||||
cd docs
|
||||
make html
|
||||
make latexpdf
|
||||
```
|
||||
|
||||
298
docs/make.bat
298
docs/make.bat
@ -1,263 +1,35 @@
|
||||
@ECHO OFF
|
||||
|
||||
REM Command file for Sphinx documentation
|
||||
|
||||
if "%SPHINXBUILD%" == "" (
|
||||
set SPHINXBUILD=sphinx-build
|
||||
)
|
||||
set BUILDDIR=_build
|
||||
set ALLSPHINXOPTS=-d %BUILDDIR%/doctrees %SPHINXOPTS% .
|
||||
set I18NSPHINXOPTS=%SPHINXOPTS% .
|
||||
if NOT "%PAPER%" == "" (
|
||||
set ALLSPHINXOPTS=-D latex_paper_size=%PAPER% %ALLSPHINXOPTS%
|
||||
set I18NSPHINXOPTS=-D latex_paper_size=%PAPER% %I18NSPHINXOPTS%
|
||||
)
|
||||
|
||||
if "%1" == "" goto help
|
||||
|
||||
if "%1" == "help" (
|
||||
:help
|
||||
echo.Please use `make ^<target^>` where ^<target^> is one of
|
||||
echo. html to make standalone HTML files
|
||||
echo. dirhtml to make HTML files named index.html in directories
|
||||
echo. singlehtml to make a single large HTML file
|
||||
echo. pickle to make pickle files
|
||||
echo. json to make JSON files
|
||||
echo. htmlhelp to make HTML files and a HTML help project
|
||||
echo. qthelp to make HTML files and a qthelp project
|
||||
echo. devhelp to make HTML files and a Devhelp project
|
||||
echo. epub to make an epub
|
||||
echo. latex to make LaTeX files, you can set PAPER=a4 or PAPER=letter
|
||||
echo. text to make text files
|
||||
echo. man to make manual pages
|
||||
echo. texinfo to make Texinfo files
|
||||
echo. gettext to make PO message catalogs
|
||||
echo. changes to make an overview over all changed/added/deprecated items
|
||||
echo. xml to make Docutils-native XML files
|
||||
echo. pseudoxml to make pseudoxml-XML files for display purposes
|
||||
echo. linkcheck to check all external links for integrity
|
||||
echo. doctest to run all doctests embedded in the documentation if enabled
|
||||
echo. coverage to run coverage check of the documentation if enabled
|
||||
goto end
|
||||
)
|
||||
|
||||
if "%1" == "clean" (
|
||||
for /d %%i in (%BUILDDIR%\*) do rmdir /q /s %%i
|
||||
del /q /s %BUILDDIR%\*
|
||||
goto end
|
||||
)
|
||||
|
||||
|
||||
REM Check if sphinx-build is available and fallback to Python version if any
|
||||
%SPHINXBUILD% 2> nul
|
||||
if errorlevel 9009 goto sphinx_python
|
||||
goto sphinx_ok
|
||||
|
||||
:sphinx_python
|
||||
|
||||
set SPHINXBUILD=python -m sphinx.__init__
|
||||
%SPHINXBUILD% 2> nul
|
||||
if errorlevel 9009 (
|
||||
echo.
|
||||
echo.The 'sphinx-build' command was not found. Make sure you have Sphinx
|
||||
echo.installed, then set the SPHINXBUILD environment variable to point
|
||||
echo.to the full path of the 'sphinx-build' executable. Alternatively you
|
||||
echo.may add the Sphinx directory to PATH.
|
||||
echo.
|
||||
echo.If you don't have Sphinx installed, grab it from
|
||||
echo.https://www.sphinx-doc.org/
|
||||
exit /b 1
|
||||
)
|
||||
|
||||
:sphinx_ok
|
||||
|
||||
|
||||
if "%1" == "html" (
|
||||
%SPHINXBUILD% -b html %ALLSPHINXOPTS% %BUILDDIR%/html
|
||||
if errorlevel 1 exit /b 1
|
||||
echo.
|
||||
echo.Build finished. The HTML pages are in %BUILDDIR%/html.
|
||||
goto end
|
||||
)
|
||||
|
||||
if "%1" == "dirhtml" (
|
||||
%SPHINXBUILD% -b dirhtml %ALLSPHINXOPTS% %BUILDDIR%/dirhtml
|
||||
if errorlevel 1 exit /b 1
|
||||
echo.
|
||||
echo.Build finished. The HTML pages are in %BUILDDIR%/dirhtml.
|
||||
goto end
|
||||
)
|
||||
|
||||
if "%1" == "singlehtml" (
|
||||
%SPHINXBUILD% -b singlehtml %ALLSPHINXOPTS% %BUILDDIR%/singlehtml
|
||||
if errorlevel 1 exit /b 1
|
||||
echo.
|
||||
echo.Build finished. The HTML pages are in %BUILDDIR%/singlehtml.
|
||||
goto end
|
||||
)
|
||||
|
||||
if "%1" == "pickle" (
|
||||
%SPHINXBUILD% -b pickle %ALLSPHINXOPTS% %BUILDDIR%/pickle
|
||||
if errorlevel 1 exit /b 1
|
||||
echo.
|
||||
echo.Build finished; now you can process the pickle files.
|
||||
goto end
|
||||
)
|
||||
|
||||
if "%1" == "json" (
|
||||
%SPHINXBUILD% -b json %ALLSPHINXOPTS% %BUILDDIR%/json
|
||||
if errorlevel 1 exit /b 1
|
||||
echo.
|
||||
echo.Build finished; now you can process the JSON files.
|
||||
goto end
|
||||
)
|
||||
|
||||
if "%1" == "htmlhelp" (
|
||||
%SPHINXBUILD% -b htmlhelp %ALLSPHINXOPTS% %BUILDDIR%/htmlhelp
|
||||
if errorlevel 1 exit /b 1
|
||||
echo.
|
||||
echo.Build finished; now you can run HTML Help Workshop with the ^
|
||||
.hhp project file in %BUILDDIR%/htmlhelp.
|
||||
goto end
|
||||
)
|
||||
|
||||
if "%1" == "qthelp" (
|
||||
%SPHINXBUILD% -b qthelp %ALLSPHINXOPTS% %BUILDDIR%/qthelp
|
||||
if errorlevel 1 exit /b 1
|
||||
echo.
|
||||
echo.Build finished; now you can run "qcollectiongenerator" with the ^
|
||||
.qhcp project file in %BUILDDIR%/qthelp, like this:
|
||||
echo.^> qcollectiongenerator %BUILDDIR%\qthelp\IdrisManual.qhcp
|
||||
echo.To view the help file:
|
||||
echo.^> assistant -collectionFile %BUILDDIR%\qthelp\IdrisManual.ghc
|
||||
goto end
|
||||
)
|
||||
|
||||
if "%1" == "devhelp" (
|
||||
%SPHINXBUILD% -b devhelp %ALLSPHINXOPTS% %BUILDDIR%/devhelp
|
||||
if errorlevel 1 exit /b 1
|
||||
echo.
|
||||
echo.Build finished.
|
||||
goto end
|
||||
)
|
||||
|
||||
if "%1" == "epub" (
|
||||
%SPHINXBUILD% -b epub %ALLSPHINXOPTS% %BUILDDIR%/epub
|
||||
if errorlevel 1 exit /b 1
|
||||
echo.
|
||||
echo.Build finished. The epub file is in %BUILDDIR%/epub.
|
||||
goto end
|
||||
)
|
||||
|
||||
if "%1" == "latex" (
|
||||
%SPHINXBUILD% -b latex %ALLSPHINXOPTS% %BUILDDIR%/latex
|
||||
if errorlevel 1 exit /b 1
|
||||
echo.
|
||||
echo.Build finished; the LaTeX files are in %BUILDDIR%/latex.
|
||||
goto end
|
||||
)
|
||||
|
||||
if "%1" == "latexpdf" (
|
||||
%SPHINXBUILD% -b latex %ALLSPHINXOPTS% %BUILDDIR%/latex
|
||||
cd %BUILDDIR%/latex
|
||||
make all-pdf
|
||||
cd %~dp0
|
||||
echo.
|
||||
echo.Build finished; the PDF files are in %BUILDDIR%/latex.
|
||||
goto end
|
||||
)
|
||||
|
||||
if "%1" == "latexpdfja" (
|
||||
%SPHINXBUILD% -b latex %ALLSPHINXOPTS% %BUILDDIR%/latex
|
||||
cd %BUILDDIR%/latex
|
||||
make all-pdf-ja
|
||||
cd %~dp0
|
||||
echo.
|
||||
echo.Build finished; the PDF files are in %BUILDDIR%/latex.
|
||||
goto end
|
||||
)
|
||||
|
||||
if "%1" == "text" (
|
||||
%SPHINXBUILD% -b text %ALLSPHINXOPTS% %BUILDDIR%/text
|
||||
if errorlevel 1 exit /b 1
|
||||
echo.
|
||||
echo.Build finished. The text files are in %BUILDDIR%/text.
|
||||
goto end
|
||||
)
|
||||
|
||||
if "%1" == "man" (
|
||||
%SPHINXBUILD% -b man %ALLSPHINXOPTS% %BUILDDIR%/man
|
||||
if errorlevel 1 exit /b 1
|
||||
echo.
|
||||
echo.Build finished. The manual pages are in %BUILDDIR%/man.
|
||||
goto end
|
||||
)
|
||||
|
||||
if "%1" == "texinfo" (
|
||||
%SPHINXBUILD% -b texinfo %ALLSPHINXOPTS% %BUILDDIR%/texinfo
|
||||
if errorlevel 1 exit /b 1
|
||||
echo.
|
||||
echo.Build finished. The Texinfo files are in %BUILDDIR%/texinfo.
|
||||
goto end
|
||||
)
|
||||
|
||||
if "%1" == "gettext" (
|
||||
%SPHINXBUILD% -b gettext %I18NSPHINXOPTS% %BUILDDIR%/locale
|
||||
if errorlevel 1 exit /b 1
|
||||
echo.
|
||||
echo.Build finished. The message catalogs are in %BUILDDIR%/locale.
|
||||
goto end
|
||||
)
|
||||
|
||||
if "%1" == "changes" (
|
||||
%SPHINXBUILD% -b changes %ALLSPHINXOPTS% %BUILDDIR%/changes
|
||||
if errorlevel 1 exit /b 1
|
||||
echo.
|
||||
echo.The overview file is in %BUILDDIR%/changes.
|
||||
goto end
|
||||
)
|
||||
|
||||
if "%1" == "linkcheck" (
|
||||
%SPHINXBUILD% -b linkcheck %ALLSPHINXOPTS% %BUILDDIR%/linkcheck
|
||||
if errorlevel 1 exit /b 1
|
||||
echo.
|
||||
echo.Link check complete; look for any errors in the above output ^
|
||||
or in %BUILDDIR%/linkcheck/output.txt.
|
||||
goto end
|
||||
)
|
||||
|
||||
if "%1" == "doctest" (
|
||||
%SPHINXBUILD% -b doctest %ALLSPHINXOPTS% %BUILDDIR%/doctest
|
||||
if errorlevel 1 exit /b 1
|
||||
echo.
|
||||
echo.Testing of doctests in the sources finished, look at the ^
|
||||
results in %BUILDDIR%/doctest/output.txt.
|
||||
goto end
|
||||
)
|
||||
|
||||
if "%1" == "coverage" (
|
||||
%SPHINXBUILD% -b coverage %ALLSPHINXOPTS% %BUILDDIR%/coverage
|
||||
if errorlevel 1 exit /b 1
|
||||
echo.
|
||||
echo.Testing of coverage in the sources finished, look at the ^
|
||||
results in %BUILDDIR%/coverage/python.txt.
|
||||
goto end
|
||||
)
|
||||
|
||||
if "%1" == "xml" (
|
||||
%SPHINXBUILD% -b xml %ALLSPHINXOPTS% %BUILDDIR%/xml
|
||||
if errorlevel 1 exit /b 1
|
||||
echo.
|
||||
echo.Build finished. The XML files are in %BUILDDIR%/xml.
|
||||
goto end
|
||||
)
|
||||
|
||||
if "%1" == "pseudoxml" (
|
||||
%SPHINXBUILD% -b pseudoxml %ALLSPHINXOPTS% %BUILDDIR%/pseudoxml
|
||||
if errorlevel 1 exit /b 1
|
||||
echo.
|
||||
echo.Build finished. The pseudo-XML files are in %BUILDDIR%/pseudoxml.
|
||||
goto end
|
||||
)
|
||||
|
||||
:end
|
||||
@ECHO OFF
|
||||
|
||||
pushd %~dp0
|
||||
|
||||
REM Command file for Sphinx documentation
|
||||
|
||||
if "%SPHINXBUILD%" == "" (
|
||||
set SPHINXBUILD=sphinx-build
|
||||
)
|
||||
set SOURCEDIR=source
|
||||
set BUILDDIR=build
|
||||
|
||||
if "%1" == "" goto help
|
||||
|
||||
%SPHINXBUILD% >NUL 2>NUL
|
||||
if errorlevel 9009 (
|
||||
echo.
|
||||
echo.The 'sphinx-build' command was not found. Make sure you have Sphinx
|
||||
echo.installed, then set the SPHINXBUILD environment variable to point
|
||||
echo.to the full path of the 'sphinx-build' executable. Alternatively you
|
||||
echo.may add the Sphinx directory to PATH.
|
||||
echo.
|
||||
echo.If you don't have Sphinx installed, grab it from
|
||||
echo.http://sphinx-doc.org/
|
||||
exit /b 1
|
||||
)
|
||||
|
||||
%SPHINXBUILD% -M %1 %SOURCEDIR% %BUILDDIR% %SPHINXOPTS% %O%
|
||||
goto end
|
||||
|
||||
:help
|
||||
%SPHINXBUILD% -M help %SOURCEDIR% %BUILDDIR% %SPHINXOPTS% %O%
|
||||
|
||||
:end
|
||||
popd
|
||||
|
||||
@ -1,4 +1,4 @@
|
||||
.. _proofs-index:
|
||||
.. _app-index:
|
||||
|
||||
################################
|
||||
Structuring Idris 2 Applications
|
||||
@ -1,32 +1,42 @@
|
||||
# -*- coding: utf-8 -*-
|
||||
# Configuration file for the Sphinx documentation builder.
|
||||
#
|
||||
# Idris Manual documentation build configuration file, created by
|
||||
# sphinx-quickstart on Sat Feb 28 20:41:47 2015.
|
||||
# Idris Manual documentation build configuration file, created by
|
||||
# sphinx-quickstart on Apr 13, 2020.
|
||||
#
|
||||
# This file is execfile()d with the current directory set to its
|
||||
# containing dir.
|
||||
#
|
||||
# Note that not all possible configuration values are present in this
|
||||
# autogenerated file.
|
||||
#
|
||||
# All configuration values have a default; values that are commented out
|
||||
# serve to show the default.
|
||||
# This file only contains a selection of the most common options. For a full
|
||||
# list see the documentation:
|
||||
# https://www.sphinx-doc.org/en/master/usage/configuration.html
|
||||
|
||||
import sys
|
||||
import os
|
||||
|
||||
# True if the readthedocs theme is locally installed
|
||||
on_rtd = os.environ.get('READTHEDOCS', None) == 'True'
|
||||
# -- Path setup --------------------------------------------------------------
|
||||
|
||||
# If extensions (or modules to document with autodoc) are in another directory,
|
||||
# add these directories to sys.path here. If the directory is relative to the
|
||||
# documentation root, use os.path.abspath to make it absolute, like shown here.
|
||||
#sys.path.insert(0, os.path.abspath('.'))
|
||||
#
|
||||
import os
|
||||
import sys
|
||||
import sphinx_rtd_theme
|
||||
# sys.path.insert(0, os.path.abspath('.'))
|
||||
|
||||
# -- General configuration ------------------------------------------------
|
||||
|
||||
# If your documentation needs a minimal Sphinx version, state it here.
|
||||
#needs_sphinx = '1.0'
|
||||
# -- Project information -----------------------------------------------------
|
||||
|
||||
# General information about the project.
|
||||
project = 'Idris2'
|
||||
copyright = '2020, The Idris Community'
|
||||
author = 'The Idris Community'
|
||||
|
||||
# The short X.Y version.
|
||||
version = '0.0'
|
||||
|
||||
# The full version, including alpha/beta/rc tags
|
||||
release = '0.0'
|
||||
|
||||
|
||||
# -- General configuration ---------------------------------------------------
|
||||
|
||||
# Add any Sphinx extension module names here, as strings. They can be
|
||||
# extensions coming with Sphinx (named 'sphinx.ext.*') or your custom
|
||||
@ -35,183 +45,40 @@ extensions = [
|
||||
'sphinx.ext.todo',
|
||||
# 'sphinx.ext.pngmath', # imgmath is not supported on readthedocs.
|
||||
'sphinx.ext.ifconfig',
|
||||
'recommonmark'
|
||||
"sphinx_rtd_theme",
|
||||
]
|
||||
|
||||
# Add any paths that contain templates here, relative to this directory.
|
||||
templates_path = ['_templates']
|
||||
|
||||
# The suffix of source filenames.
|
||||
source_suffix = ['.rst','.md']
|
||||
# List of patterns, relative to source directory, that match files and
|
||||
# directories to ignore when looking for source files.
|
||||
# This pattern also affects html_static_path and html_extra_path.
|
||||
exclude_patterns = []
|
||||
|
||||
# The encoding of source files.
|
||||
#source_encoding = 'utf-8-sig'
|
||||
|
||||
# -- Options for HTML output -------------------------------------------------
|
||||
|
||||
# The master toctree document.
|
||||
master_doc = 'index'
|
||||
|
||||
# General information about the project.
|
||||
project = u'Idris2'
|
||||
copyright = u'2019, The Idris Community'
|
||||
author = u'The Idris Community'
|
||||
|
||||
# The version info for the project you're documenting, acts as replacement for
|
||||
# |version| and |release|, also used in various other places throughout the
|
||||
# built documents.
|
||||
#
|
||||
# The short X.Y version.
|
||||
version = '0.0'
|
||||
# The full version, including alpha/beta/rc tags.
|
||||
release = '0.0'
|
||||
|
||||
# The language for content autogenerated by Sphinx. Refer to documentation
|
||||
# for a list of supported languages.
|
||||
#
|
||||
# This is also used if you do content translation via gettext catalogs.
|
||||
# Usually you set "language" from the command line for these cases.
|
||||
language = None
|
||||
|
||||
# There are two options for replacing |today|: either, you set today to some
|
||||
# non-false value, then it is used:
|
||||
#today = ''
|
||||
# Else, today_fmt is used as the format for a strftime call.
|
||||
#today_fmt = '%B %d, %Y'
|
||||
|
||||
# List of patterns, relative to source directory, that match files and
|
||||
# directories to ignore when looking for source files.
|
||||
exclude_patterns = ['_build']
|
||||
|
||||
# The reST default role (used for this markup: `text`) to use for all
|
||||
# documents.
|
||||
#default_role = None
|
||||
|
||||
# If true, '()' will be appended to :func: etc. cross-reference text.
|
||||
#add_function_parentheses = True
|
||||
|
||||
# If true, the current module name will be prepended to all description
|
||||
# unit titles (such as .. function::).
|
||||
#add_module_names = True
|
||||
|
||||
# If true, sectionauthor and moduleauthor directives will be shown in the
|
||||
# output. They are ignored by default.
|
||||
#show_authors = False
|
||||
|
||||
# The name of the Pygments (syntax highlighting) style to use.
|
||||
pygments_style = 'sphinx'
|
||||
|
||||
# A list of ignored prefixes for module index sorting.
|
||||
#modindex_common_prefix = []
|
||||
|
||||
# If true, keep warnings as "system message" paragraphs in the built documents.
|
||||
#keep_warnings = False
|
||||
|
||||
# If true, `todo` and `todoList` produce output, else they produce nothing.
|
||||
todo_include_todos = True
|
||||
|
||||
|
||||
# -- Options for HTML output ----------------------------------------------
|
||||
|
||||
# The theme to use for HTML and HTML Help pages. See the documentation for
|
||||
# a list of builtin themes.
|
||||
html_theme = "default"
|
||||
# # Read The Docs Themes specific settings
|
||||
html_theme = 'sphinx_rtd_theme'
|
||||
html_theme_options = {
|
||||
'display_version': True,
|
||||
'prev_next_buttons_location': 'bottom'
|
||||
}
|
||||
|
||||
if not on_rtd: # only import and set the theme if we're building docs locally
|
||||
try:
|
||||
import sphinx_rtd_theme
|
||||
html_theme = 'sphinx_rtd_theme'
|
||||
html_theme_path = [sphinx_rtd_theme.get_html_theme_path()]
|
||||
except ImportError:
|
||||
html_theme = "default"
|
||||
|
||||
# Theme options are theme-specific and customize the look and feel of a theme
|
||||
# further. For a list of options available for each theme, see the
|
||||
# documentation.
|
||||
#html_theme_options = {}
|
||||
|
||||
# Add any paths that contain custom themes here, relative to this directory.
|
||||
#html_theme_path = []
|
||||
|
||||
# The name for this set of Sphinx documents. If None, it defaults to
|
||||
# "<project> v<release> documentation".
|
||||
#html_title = None
|
||||
|
||||
# A shorter title for the navigation bar. Default is the same as html_title.
|
||||
#html_short_title = None
|
||||
|
||||
# The name of an image file (relative to this directory) to place at the top
|
||||
# of the sidebar.
|
||||
#html_logo = None
|
||||
|
||||
# The name of an image file (within the static path) to use as favicon of the
|
||||
# docs. This file should be a Windows icon file (.ico) being 16x16 or 32x32
|
||||
# pixels large.
|
||||
#html_favicon = None
|
||||
|
||||
# Add any paths that contain custom static files (such as style sheets) here,
|
||||
# relative to this directory. They are copied after the builtin static files,
|
||||
# so a file named "default.css" will overwrite the builtin "default.css".
|
||||
html_static_path = ['_static']
|
||||
|
||||
# Add any extra paths that contain custom files (such as robots.txt or
|
||||
# .htaccess) here, relative to this directory. These files are copied
|
||||
# directly to the root of the documentation.
|
||||
#html_extra_path = []
|
||||
|
||||
# If not '', a 'Last updated on:' timestamp is inserted at every page bottom,
|
||||
# using the given strftime format.
|
||||
#html_last_updated_fmt = '%b %d, %Y'
|
||||
|
||||
# If true, SmartyPants will be used to convert quotes and dashes to
|
||||
# typographically correct entities.
|
||||
#html_use_smartypants = True
|
||||
|
||||
# Custom sidebar templates, maps document names to template names.
|
||||
#html_sidebars = {}
|
||||
|
||||
# Additional templates that should be rendered to pages, maps page names to
|
||||
# template names.
|
||||
#html_additional_pages = {}
|
||||
|
||||
# If false, no module index is generated.
|
||||
#html_domain_indices = True
|
||||
|
||||
# If false, no index is generated.
|
||||
#html_use_index = True
|
||||
|
||||
# If true, the index is split into individual pages for each letter.
|
||||
#html_split_index = False
|
||||
|
||||
# If true, links to the reST sources are added to the pages.
|
||||
#html_show_sourcelink = True
|
||||
|
||||
# If true, "Created using Sphinx" is shown in the HTML footer. Default is True.
|
||||
#html_show_sphinx = True
|
||||
|
||||
# If true, "(C) Copyright ..." is shown in the HTML footer. Default is True.
|
||||
#html_show_copyright = True
|
||||
|
||||
# If true, an OpenSearch description file will be output, and all pages will
|
||||
# contain a <link> tag referring to it. The value of this option must be the
|
||||
# base URL from which the finished HTML is served.
|
||||
#html_use_opensearch = ''
|
||||
|
||||
# This is the file name suffix for HTML files (e.g. ".xhtml").
|
||||
#html_file_suffix = None
|
||||
|
||||
# Language to be used for generating the HTML full-text search index.
|
||||
# Sphinx supports the following languages:
|
||||
# 'da', 'de', 'en', 'es', 'fi', 'fr', 'hu', 'it', 'ja'
|
||||
# 'nl', 'no', 'pt', 'ro', 'ru', 'sv', 'tr'
|
||||
#html_search_language = 'en'
|
||||
|
||||
# A dictionary with options for the search language support, empty by default.
|
||||
# Now only 'ja' uses this config value
|
||||
#html_search_options = {'type': 'default'}
|
||||
|
||||
# The name of a javascript file (relative to the configuration directory) that
|
||||
# implements a search results scorer. If empty, the default will be used.
|
||||
#html_search_scorer = 'scorer.js'
|
||||
|
||||
# Output file base name for HTML help builder.
|
||||
htmlhelp_basename = 'IdrisManualdoc'
|
||||
|
||||
@ -305,7 +172,7 @@ latex_show_url = 'footnote'
|
||||
|
||||
# The name of an image file (relative to this directory) to place at the top of
|
||||
# the title page.
|
||||
latex_logo = '../icons/idris-512x512.png'
|
||||
latex_logo = '../../icons/idris-512x512.png'
|
||||
|
||||
# For "manual" documents, if this is true, then toplevel headings are parts,
|
||||
# not chapters.
|
||||
@ -7,33 +7,35 @@ Further Reading
|
||||
Further information about Idris programming, and programming with
|
||||
dependent types in general, can be obtained from various sources:
|
||||
|
||||
- `Type-Driven Development with Idris <https://www.manning.com/books/type-driven-development-with-idris>`_
|
||||
* `Type-Driven Development with Idris <https://www.manning.com/books/type-driven-development-with-idris>`_
|
||||
by Edwin Brady, available from `Manning <https://www.manning.com>`_.
|
||||
|
||||
- The Idris web site (http://www.idris-lang.org/) and by asking
|
||||
* The Idris web site (http://www.idris-lang.org/) and by asking
|
||||
questions on the mailing list.
|
||||
|
||||
- The IRC channel ``#idris``, on
|
||||
* The IRC channel ``#idris``, on
|
||||
`webchat.freenode.net <https://webchat.freenode.net/>`__.
|
||||
|
||||
- The wiki (https://github.com/idris-lang/Idris-dev/wiki/) has further
|
||||
* The wiki (https://github.com/idris-lang/Idris-dev/wiki/) has further
|
||||
user provided information, in particular:
|
||||
|
||||
- https://github.com/idris-lang/Idris-dev/wiki/Manual
|
||||
* https://github.com/idris-lang/Idris-dev/wiki/Manual
|
||||
|
||||
- https://github.com/idris-lang/Idris-dev/wiki/Language-Features
|
||||
* https://github.com/idris-lang/Idris-dev/wiki/Language-Features
|
||||
|
||||
- Examining the prelude and exploring the ``samples`` in the
|
||||
* Examining the prelude and exploring the ``samples`` in the
|
||||
distribution. The Idris 2 source can be found online at:
|
||||
https://github.com/edwinb/Idris2.
|
||||
|
||||
* https://github.com/edwinb/Idris2.
|
||||
|
||||
- Existing projects on the ``Idris Hackers`` web space:
|
||||
http://idris-hackers.github.io.
|
||||
* Existing projects on the ``Idris Hackers`` web space:
|
||||
|
||||
* http://idris-hackers.github.io.
|
||||
|
||||
- Various papers (e.g. [1]_, [2]_, and [3]_). Although these mostly
|
||||
* Various papers (e.g. [#BradyHammond2012]_, [#Brady]_, and [#BradyHammond2010]_). Although these mostly
|
||||
describe older versions of Idris.
|
||||
|
||||
.. [1] Edwin Brady and Kevin Hammond. 2012. Resource-Safe systems
|
||||
.. [#BradyHammond2012] Edwin Brady and Kevin Hammond. 2012. Resource-Safe systems
|
||||
programming with embedded domain specific languages. In
|
||||
Proceedings of the 14th international conference on Practical
|
||||
Aspects of Declarative Languages (PADL'12), Claudio Russo and
|
||||
@ -41,14 +43,14 @@ dependent types in general, can be obtained from various sources:
|
||||
242-257. DOI=10.1007/978-3-642-27694-1_18
|
||||
http://dx.doi.org/10.1007/978-3-642-27694-1_18
|
||||
|
||||
.. [2] Edwin C. Brady. 2011. IDRIS ---: systems programming meets full
|
||||
.. [#Brady] Edwin C. Brady. 2011. IDRIS ---: systems programming meets full
|
||||
dependent types. In Proceedings of the 5th ACM workshop on
|
||||
Programming languages meets program verification (PLPV
|
||||
'11). ACM, New York, NY, USA,
|
||||
43-54. DOI=10.1145/1929529.1929536
|
||||
http://doi.acm.org/10.1145/1929529.1929536
|
||||
|
||||
.. [3] Edwin C. Brady and Kevin Hammond. 2010. Scrapping your
|
||||
.. [#BradyHammond2010] Edwin C. Brady and Kevin Hammond. 2010. Scrapping your
|
||||
inefficient engine: using partial evaluation to improve
|
||||
domain-specific language implementation. In Proceedings of the
|
||||
15th ACM SIGPLAN international conference on Functional
|
||||
@ -165,7 +165,7 @@ then ``:ps 96 vzipWith_rhs_1`` will give
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
[]
|
||||
[]
|
||||
|
||||
This works because it is searching for a ``Vect`` of length 0, of
|
||||
which the empty vector is the only possibility. Similarly, and perhaps
|
||||
@ -164,7 +164,7 @@ see this at the REPL:
|
||||
Main> :t Ord
|
||||
Prelude.Ord : Type -> Type
|
||||
|
||||
So, ``(Ord a, Show a)`` is an ordinary pair of ``Type``s, with two constraints
|
||||
So, ``(Ord a, Show a)`` is an ordinary pair of ``Types``, with two constraints
|
||||
as the first and second element of the pair.
|
||||
|
||||
Note: Interfaces and ``mutual`` blocks
|
||||
@ -434,7 +434,7 @@ Idiom brackets
|
||||
While ``do`` notation gives an alternative meaning to sequencing,
|
||||
idioms give an alternative meaning to *application*. The notation and
|
||||
larger example in this section is inspired by Conor McBride and Ross
|
||||
Paterson’s paper “Applicative Programming with Effects” [1]_.
|
||||
Paterson’s paper “Applicative Programming with Effects” [#ConorRoss]_.
|
||||
|
||||
First, let us revisit ``m_add`` above. All it is really doing is
|
||||
applying an operator to two values extracted from ``Maybe Int``. We
|
||||
@ -470,19 +470,19 @@ above (this is defined in the Idris library):
|
||||
_ <*> _ = Nothing
|
||||
|
||||
Using ``<*>`` we can use this implementation as follows, where a function
|
||||
application ``[| f a1 …an |]`` is translated into ``pure f <*> a1 <*>
|
||||
application ``[ f a1 …an |]`` is translated into ``pure f <*> a1 <*>
|
||||
… <*> an``:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
m_add' : Maybe Int -> Maybe Int -> Maybe Int
|
||||
m_add' x y = [| x + y |]
|
||||
m_add' x y = [ x + y |]
|
||||
|
||||
An error-handling interpreter
|
||||
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
|
||||
Idiom notation is commonly useful when defining evaluators. McBride
|
||||
and Paterson describe such an evaluator [1]_, for a language similar
|
||||
and Paterson describe such an evaluator [#ConorRoss]_, for a language similar
|
||||
to the following:
|
||||
|
||||
.. code-block:: idris
|
||||
@ -655,7 +655,7 @@ is declared with the ``| m`` after the interface declaration. We call ``m`` a
|
||||
parameter used to find an implementation.
|
||||
|
||||
|
||||
.. [1] Conor McBride and Ross Paterson. 2008. Applicative programming
|
||||
.. [#ConorRoss] Conor McBride and Ross Paterson. 2008. Applicative programming
|
||||
with effects. J. Funct. Program. 18, 1 (January 2008),
|
||||
1-13. DOI=10.1017/S0956796807006326
|
||||
http://dx.doi.org/10.1017/S0956796807006326
|
||||
@ -21,7 +21,7 @@ In a language with *dependent types*, however, the distinction is less
|
||||
clear. Dependent types allow types to “depend” on values — in other
|
||||
words, types are a *first class* language construct and can be
|
||||
manipulated like any other value. The standard example is the type of
|
||||
lists of a given length [1]_, ``Vect n a``, where ``a`` is the element
|
||||
lists of a given length [#fn1]_, ``Vect n a``, where ``a`` is the element
|
||||
type and ``n`` is the length of the list and can be an arbitrary term.
|
||||
|
||||
When types can contain values, and where those values describe
|
||||
@ -69,6 +69,7 @@ so that you can try them out easily. They can be found under
|
||||
``samples``. It is, however, strongly recommended that you type
|
||||
them in yourself, rather than simply loading and reading them.
|
||||
|
||||
.. [1]
|
||||
Typically, and perhaps confusingly, referred to in the dependently
|
||||
typed programming literature as “vectors”
|
||||
.. rubric:: Footnotes
|
||||
|
||||
.. [#fn1] Typically, and perhaps confusingly, referred to in the dependently
|
||||
typed programming literature as "vectors".
|
||||
@ -14,7 +14,7 @@ Implicit arguments
|
||||
==================
|
||||
|
||||
We have already seen implicit arguments, which allows arguments to be
|
||||
omitted when they can be inferred by the type checker, e.g.
|
||||
omitted when they can be inferred by the type checker [#IdrisType]_, e.g.
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
@ -101,6 +101,7 @@ 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
|
||||
|
||||
@ -161,5 +162,4 @@ The application of ``myid`` to itself leads to a cycle in the universe
|
||||
hierarchy — ``myid``\ ’s first argument is a ``Type``, which cannot be
|
||||
at a lower level than required if it is applied to itself.
|
||||
|
||||
.. [1]
|
||||
https://github.com/david-christiansen/idris-type-providers
|
||||
.. [#IdrisType] https://github.com/david-christiansen/idris-type-providers
|
||||
@ -148,6 +148,7 @@ 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
|
||||
|
||||
@ -97,7 +97,7 @@ real distinction between proofs and programs. A proof, as far as we are
|
||||
concerned here, is merely a program with a precise enough type to
|
||||
guarantee a particular property of interest.
|
||||
|
||||
We won’t go into details here, but the Curry-Howard correspondence [1]_
|
||||
We won’t go into details here, but the Curry-Howard correspondence [#Timothy]_
|
||||
explains this relationship. The proof itself is immediate, because
|
||||
``plus Z n`` normalises to ``n`` by the definition of ``plus``:
|
||||
|
||||
@ -450,7 +450,7 @@ example from a C library) where totality can be shown by an external
|
||||
argument.
|
||||
|
||||
|
||||
.. [1] Timothy G. Griffin. 1989. A formulae-as-type notion of
|
||||
.. [#Timothy] Timothy G. Griffin. 1989. A formulae-as-type notion of
|
||||
control. In Proceedings of the 17th ACM SIGPLAN-SIGACT
|
||||
symposium on Principles of programming languages (POPL
|
||||
'90). ACM, New York, NY, USA, 47-58. DOI=10.1145/96709.96714
|
||||
@ -31,7 +31,7 @@ The ``with`` rule — matching intermediate values
|
||||
|
||||
Very often, we need to match on the result of an intermediate
|
||||
computation. Idris provides a construct for this, the ``with``
|
||||
rule, inspired by views in ``Epigram`` [1]_, which takes account of
|
||||
rule, inspired by views in ``Epigram`` [#McBridgeMcKinna]_, which takes account of
|
||||
the fact that matching on a value in a dependently typed language can
|
||||
affect what we know about the forms of other values. In its simplest
|
||||
form, the ``with`` rule adds another argument to the function being
|
||||
@ -151,6 +151,6 @@ it is:
|
||||
For full details on ``rewrite`` in particular, please refer to the theorem
|
||||
proving tutorial, in Section :ref:`proofs-index`.
|
||||
|
||||
.. [1] Conor McBride and James McKinna. 2004. The view from the
|
||||
.. [#McBridgeMcKinna] Conor McBride and James McKinna. 2004. The view from the
|
||||
left. J. Funct. Program. 14, 1 (January 2004),
|
||||
69-111. https://doi.org/10.1017/S0956796803004829
|
||||
@ -263,7 +263,7 @@ Idris 1, it won't attempt significant backtracking. If you have deeply nested
|
||||
ambiguous names (beyond a small threshold, default 3) Idris 2 will report an
|
||||
error. You can change this threshold with a directive, for example:
|
||||
|
||||
.. code_block:: idris
|
||||
.. code-block:: idris
|
||||
|
||||
%ambiguity_depth 10
|
||||
|
||||
Loading…
Reference in New Issue
Block a user