mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-08-16 12:10:39 +03:00
use HTTPS URL instead of HTTP URL when possible
This commit is contained in:
Milan Kral
parent
4d8d85de7b
commit
35757f928a
@ -17,7 +17,7 @@ If you use `Idris` in your work we would prefer it if you would use the followin
|
||||
pages = {552--593},
|
||||
numpages = {42},
|
||||
doi = {10.1017/S095679681300018X},
|
||||
URL = {http://journals.cambridge.org/article_S095679681300018X},
|
||||
URL = {https://journals.cambridge.org/article_S095679681300018X},
|
||||
}
|
||||
```
|
||||
|
||||
|
||||
@ -6,9 +6,9 @@ Here are a few guidelines that we would like contributors to follow so that we c
|
||||
|
||||
## Getting Started
|
||||
|
||||
1. Make sure you are familiar with [Git](http://git-scm.com/book).
|
||||
1. Make sure you are familiar with [Git](https://git-scm.com/book).
|
||||
1. Make sure you have a [GitHub account](https://github.com/signup/free).
|
||||
1. Make sure you are familiar with: [Idris](http://eb.host.cs.st-andrews.ac.uk/writings/idris-tutorial.pdf).
|
||||
1. Make sure you are familiar with: [Idris](https://eb.host.cs.st-andrews.ac.uk/writings/idris-tutorial.pdf).
|
||||
1. Make sure you can install Idris:
|
||||
* [Mac OS X](https://github.com/idris-lang/Idris-dev/wiki/Idris-on-OS-X-using-Homebrew)
|
||||
* [Ubuntu](https://github.com/idris-lang/Idris-dev/wiki/Idris-on-Ubuntu)
|
||||
@ -72,7 +72,7 @@ We do not want you wasting your time nor duplicating somebody's work!
|
||||
|
||||
## Making Changes
|
||||
|
||||
Idris developers and hackers try to adhere to something similar to the [successful git branching model](http://nvie.com/posts/a-successful-git-branching-model/).
|
||||
Idris developers and hackers try to adhere to something similar to the [successful git branching model](https://nvie.com/posts/a-successful-git-branching-model/).
|
||||
The steps are described below.
|
||||
|
||||
### New contributors
|
||||
@ -175,8 +175,8 @@ To help increase the chance of your pull request being accepted:
|
||||
* Idris FAQs: [Official](https://idris.readthedocs.io/en/latest/faq/faq.html); [Unofficial](https://github.com/idris-lang/Idris-dev/wiki/Unofficial-FAQ);
|
||||
* [Idris Manual](https://github.com/idris-lang/Idris-dev/wiki/Manual);
|
||||
* [Idris Tutorial](https://idris.readthedocs.io/en/latest/tutorial/index.html);
|
||||
* [Idris News](http://www.idris-lang.org/news/);
|
||||
* [other Idris docs](http://www.idris-lang.org/documentation/).
|
||||
* [Idris News](https://www.idris-lang.org/news/);
|
||||
* [other Idris docs](https://www.idris-lang.org/documentation/).
|
||||
* [Using Pull Requests](https://help.github.com/articles/using-pull-requests)
|
||||
* [General GitHub Documentation](https://help.github.com/).
|
||||
|
||||
|
||||
2
Makefile
2
Makefile
@ -56,7 +56,7 @@ linecount:
|
||||
|
||||
#Note: this doesn't yet link to Hackage properly
|
||||
doc: dist/setup-config
|
||||
$(CABAL) haddock --hyperlink-source --html --hoogle --html-location="http://hackage.haskell.org/packages/archive/\$$pkg/latest/doc/html" --haddock-options="--title Idris"
|
||||
$(CABAL) haddock --hyperlink-source --html --hoogle --html-location="https://hackage.haskell.org/packages/archive/\$$pkg/latest/doc/html" --haddock-options="--title Idris"
|
||||
|
||||
lib_doc:
|
||||
$(MAKE) -C libs IDRIS=../../dist/build/idris/idris doc
|
||||
|
||||
@ -4,11 +4,11 @@
|
||||
[](https://ci.appveyor.com/project/idrislang/idris-dev)
|
||||
[](https://readthedocs.org/projects/idris/?badge=latest)
|
||||
[](https://hackage.haskell.org/package/idris)
|
||||
[](http://stackage.org/lts/package/idris)
|
||||
[](http://stackage.org/nightly/package/idris)
|
||||
[](https://stackage.org/lts/package/idris)
|
||||
[](https://stackage.org/nightly/package/idris)
|
||||
[](https://www.irccloud.com/invite?channel=%23idris&hostname=irc.freenode.net&port=6697&ssl=1)
|
||||
|
||||
Idris (http://idris-lang.org/) is a general-purpose functional programming
|
||||
Idris (https://idris-lang.org/) is a general-purpose functional programming
|
||||
language with dependent types.
|
||||
|
||||
## Installation Guides.
|
||||
@ -28,7 +28,7 @@ Idris has support for external code generators. Supplied with the distribution
|
||||
is a C code generator to compile executables, and a JavaScript code generator
|
||||
with support for node.js and browser JavaScript.
|
||||
|
||||
More information about [code generators can be found on the wiki](http://idris.readthedocs.io/en/latest/reference/codegen.html).
|
||||
More information about [code generators can be found on the wiki](https://idris.readthedocs.io/en/latest/reference/codegen.html).
|
||||
|
||||
## More Information
|
||||
|
||||
|
||||
@ -5,7 +5,7 @@ init:
|
||||
|
||||
mkdir C:\ghc
|
||||
|
||||
Invoke-WebRequest "http://downloads.haskell.org/~ghc/8.4.3/ghc-8.4.3-x86_64-unknown-mingw32.tar.xz" -OutFile C:\ghc\ghc.tar.xz -UserAgent "Curl"
|
||||
Invoke-WebRequest "https://downloads.haskell.org/~ghc/8.4.3/ghc-8.4.3-x86_64-unknown-mingw32.tar.xz" -OutFile C:\ghc\ghc.tar.xz -UserAgent "Curl"
|
||||
|
||||
7z x C:\ghc\ghc.tar.xz -oC:\ghc
|
||||
|
||||
|
||||
@ -68,7 +68,7 @@ jobs:
|
||||
choco install 7zip.portable -y --no-progress
|
||||
choco install msys2 -y --no-progress --params "/InstallDir=C:/msys64/"
|
||||
mkdir C:\ghc
|
||||
Invoke-WebRequest "http://downloads.haskell.org/~ghc/8.4.3/ghc-8.4.3-x86_64-unknown-mingw32.tar.xz" -OutFile C:\ghc\ghc.tar.xz -UserAgent "Curl"
|
||||
Invoke-WebRequest "https://downloads.haskell.org/~ghc/8.4.3/ghc-8.4.3-x86_64-unknown-mingw32.tar.xz" -OutFile C:\ghc\ghc.tar.xz -UserAgent "Curl"
|
||||
7z x C:\ghc\ghc.tar.xz -oC:\ghc
|
||||
7z x C:\ghc\ghc.tar -oC:\ghc
|
||||
displayName: "Setting up environment"
|
||||
|
||||
@ -3,7 +3,7 @@ import Data.Vect
|
||||
|
||||
{- Toy program that outputs the n first digits of Pi.
|
||||
|
||||
Inspired from http://www.haskell.org/haskellwiki/Shootout/Pidigits.
|
||||
Inspired from https://www.haskell.org/haskellwiki/Shootout/Pidigits.
|
||||
The original ns and str lazy lists have been replaced by strict functions.
|
||||
|
||||
Memory usage seems to be excessive. One of the branches of str is tail recursive, and
|
||||
|
||||
@ -7,4 +7,4 @@ rights to Documentation for Idris.
|
||||
|
||||
More information concerning the CC0 can be found online at:
|
||||
|
||||
http://creativecommons.org/publicdomain/zero/1.0/
|
||||
https://creativecommons.org/publicdomain/zero/1.0/
|
||||
|
||||
@ -9,7 +9,7 @@ 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 http://sphinx-doc.org/)
|
||||
$(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.
|
||||
|
||||
@ -1,7 +1,7 @@
|
||||
# Documentation for the Idris Language.
|
||||
|
||||
|
||||
This manual has been prepared using ReStructured Text and the [Sphinx Documentation Generator](http://sphinx-doc.org) for future inclusion on [Read The Docs](http://www.readthedocs.org).
|
||||
This manual has been prepared using ReStructured Text and the [Sphinx Documentation Generator](https://www.sphinx-doc.org) for future inclusion on [Read The Docs](https://www.readthedocs.org).
|
||||
|
||||
## Dependencies
|
||||
|
||||
@ -12,7 +12,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.
|
||||
|
||||
*Note* [ReadTheDocs](http://www.readthedocs.org) works with Sphinx
|
||||
*Note* [ReadTheDocs](https://www.readthedocs.org) works with Sphinx
|
||||
`v1.2.2`. If you install a more recent version of sphinx then
|
||||
'incorrectly' marked up documentation may get passed the build system
|
||||
of readthedocs and be ignored. In the past we had several code-blocks
|
||||
@ -45,7 +45,7 @@ rights to Documentation for Idris.
|
||||
|
||||
More information concerning the CC0 can be found online at:
|
||||
|
||||
http://creativecommons.org/publicdomain/zero/1.0/
|
||||
https://creativecommons.org/publicdomain/zero/1.0/
|
||||
|
||||
|
||||
When contributing material to the manual please bear in mind that the work will be licensed as above.
|
||||
|
||||
@ -51,7 +51,7 @@ foundations are also well-studied see [5]_, [6]_, [7]_, [8]_.
|
||||
Programming Languages and Systems (APLAS '09), Zhenjiang Hu
|
||||
(Ed.). Springer-Verlag, Berlin, Heidelberg,
|
||||
95-110. DOI=10.1007/978-3-642-10672-9_9
|
||||
http://link.springer.com/chapter/10.1007%2F978-3-642-10672-9_9
|
||||
https://link.springer.com/chapter/10.1007%2F978-3-642-10672-9_9
|
||||
|
||||
|
||||
.. [4] Ohad Kammar, Sam Lindley, and Nicolas Oury. 2013. Handlers in
|
||||
|
||||
@ -25,7 +25,7 @@ A tutorial on the `Effects` package in `Idris`.
|
||||
Idris Community* has waived all copyright and related or neighbouring
|
||||
rights to Documentation for Idris.
|
||||
|
||||
More information concerning the CC0 can be found online at: http://creativecommons.org/publicdomain/zero/1.0/
|
||||
More information concerning the CC0 can be found online at: https://creativecommons.org/publicdomain/zero/1.0/
|
||||
|
||||
.. toctree::
|
||||
:maxdepth: 1
|
||||
|
||||
@ -3,7 +3,7 @@ Introduction
|
||||
************
|
||||
|
||||
Pure functional languages with dependent types such as `Idris
|
||||
<http://www.idris-lang.org/>`_ support reasoning about programs directly
|
||||
<https://www.idris-lang.org/>`_ support reasoning about programs directly
|
||||
in the type system, promising that we can *know* a program will run
|
||||
correctly (i.e. according to the specification in its type) simply
|
||||
because it compiles. Realistically, though, things are not so simple:
|
||||
|
||||
@ -37,7 +37,7 @@ Is there some documentation for the standard lib? List of functions?
|
||||
=====================================================================
|
||||
|
||||
API documentation for the shipped packages is listed on `the
|
||||
documentation page <http://www.idris-lang.org/documentation/>`_.
|
||||
documentation page <https://www.idris-lang.org/documentation/>`_.
|
||||
|
||||
Unfortunately, the default prelude and shipped packages for `Idris`
|
||||
are not necessarily complete with regards to documentation. Other
|
||||
@ -310,7 +310,7 @@ better and it will make sense to revisit this. For now, however, Idris will not
|
||||
be offering arbitrary Unicode symbols in operators.
|
||||
|
||||
This seems like an instance of `Wadler's
|
||||
Law <http://www.haskell.org/haskellwiki/Wadler%27s_Law>`__ in action.
|
||||
Law <https://www.haskell.org/haskellwiki/Wadler%27s_Law>`__ in action.
|
||||
|
||||
This answer is based on Edwin Brady's response in the following
|
||||
`pull request <https://github.com/idris-lang/Idris-dev/pull/694#issuecomment-29559291>`_.
|
||||
|
||||
@ -12,7 +12,7 @@ Tutorials submitted by community members.
|
||||
Idris Community* has waived all copyright and related or neighboring
|
||||
rights to Documentation for Idris.
|
||||
|
||||
More information concerning the CC0 can be found online at: http://creativecommons.org/publicdomain/zero/1.0/
|
||||
More information concerning the CC0 can be found online at: https://creativecommons.org/publicdomain/zero/1.0/
|
||||
|
||||
|
||||
.. toctree::
|
||||
|
||||
@ -22,7 +22,7 @@ We will be given the following prompt, in future releases the version string wil
|
||||
____ __ _
|
||||
/ _/___/ /____(_)____
|
||||
/ // __ / ___/ / ___/ Version 0.9.18.1
|
||||
_/ // /_/ / / / (__ ) http://www.idris-lang.org/
|
||||
_/ // /_/ / / / (__ ) https://www.idris-lang.org/
|
||||
/___/\__,_/_/ /_/____/ Type :? for help
|
||||
|
||||
Idris is free software with ABSOLUTELY NO WARRANTY.
|
||||
|
||||
@ -3,7 +3,7 @@ Type Providers in Idris
|
||||
***********************
|
||||
|
||||
`Type providers in Idris
|
||||
<http://www.davidchristiansen.dk/pubs/dependent-type-providers.pdf>`__
|
||||
<https://www.davidchristiansen.dk/pubs/dependent-type-providers.pdf>`__
|
||||
are simple enough, but there are a few caveats to using them that it
|
||||
would be worthwhile to go through the basic steps. We also go over
|
||||
foreign functions, because these will often be used with type
|
||||
|
||||
@ -13,7 +13,7 @@ Documentation for the Idris Language
|
||||
Idris Community* has waived all copyright and related or neighboring
|
||||
rights to Documentation for Idris.
|
||||
|
||||
More information concerning the CC0 can be found online at: http://creativecommons.org/publicdomain/zero/1.0/
|
||||
More information concerning the CC0 can be found online at: https://creativecommons.org/publicdomain/zero/1.0/
|
||||
|
||||
|
||||
.. toctree::
|
||||
|
||||
@ -2,7 +2,7 @@ $ idris hello.idr
|
||||
____ __ _
|
||||
/ _/___/ /____(_)____
|
||||
/ // __ / ___/ / ___/ Version 1.3.2
|
||||
_/ // /_/ / / / (__ ) http://www.idris-lang.org/
|
||||
_/ // /_/ / / / (__ ) https://www.idris-lang.org/
|
||||
/___/\__,_/_/ /_/____/ Type :? for help
|
||||
|
||||
Type checking ./hello.idr
|
||||
|
||||
@ -2,7 +2,7 @@ $ idris interp.idr
|
||||
____ __ _
|
||||
/ _/___/ /____(_)____
|
||||
/ // __ / ___/ / ___/ Version 1.3.2
|
||||
_/ // /_/ / / / (__ ) http://www.idris-lang.org/
|
||||
_/ // /_/ / / / (__ ) https://www.idris-lang.org/
|
||||
/___/\__,_/_/ /_/____/ Type :? for help
|
||||
|
||||
Type checking ./interp.idr
|
||||
|
||||
@ -2,7 +2,7 @@ $ idris
|
||||
____ __ _
|
||||
/ _/___/ /____(_)____
|
||||
/ // __ / ___/ / ___/ Version 1.3.2
|
||||
_/ // /_/ / / / (__ ) http://www.idris-lang.org/
|
||||
_/ // /_/ / / / (__ ) https://www.idris-lang.org/
|
||||
/___/\__,_/_/ /_/____/ Type :? for help
|
||||
|
||||
Idris>
|
||||
|
||||
@ -65,7 +65,7 @@ if errorlevel 9009 (
|
||||
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/
|
||||
echo.https://www.sphinx-doc.org/
|
||||
exit /b 1
|
||||
)
|
||||
|
||||
|
||||
@ -13,7 +13,7 @@ A tutorial on theorem proving in Idris.
|
||||
Idris Community* has waived all copyright and related or neighboring
|
||||
rights to Documentation for Idris.
|
||||
|
||||
More information concerning the CC0 can be found online at: http://creativecommons.org/publicdomain/zero/1.0/
|
||||
More information concerning the CC0 can be found online at: https://creativecommons.org/publicdomain/zero/1.0/
|
||||
|
||||
.. toctree::
|
||||
:maxdepth: 1
|
||||
|
||||
@ -129,7 +129,7 @@ On running , two global names are created, ``plusredZ_Z`` and
|
||||
|
||||
. / _/___/ /____(_)____
|
||||
/ // __ / ___/ / ___/ Version 1.2.0
|
||||
_/ // /_/ / / / (__ ) http://www.idris-lang.org/
|
||||
_/ // /_/ / / / (__ ) https://www.idris-lang.org/
|
||||
/___/\__,_/_/ /_/____/ Type :? for help
|
||||
|
||||
Idris is free software with ABSOLUTELY NO WARRANTY.
|
||||
|
||||
@ -254,7 +254,7 @@ Benchmarks
|
||||
==========
|
||||
|
||||
- source: https://github.com/ziman/idris-benchmarks
|
||||
- results: http://ziman.functor.sk/erasure-bm/
|
||||
- results: https://ziman.functor.sk/erasure-bm/
|
||||
|
||||
It can be clearly seen that asymptotics are improved by erasure.
|
||||
|
||||
@ -499,4 +499,4 @@ References
|
||||
|
||||
.. [BMM04] Edwin Brady, Conor McBride, James McKinna: `Inductive
|
||||
families need not store their indices
|
||||
<http://citeseerx.ist.psu.edu/viewdoc/summary;jsessionid=1F796FCF0F2C4C535FC70F62BE2FB821?doi=10.1.1.62.3849>`__
|
||||
<https://citeseerx.ist.psu.edu/viewdoc/summary;jsessionid=1F796FCF0F2C4C535FC70F62BE2FB821?doi=10.1.1.62.3849>`__
|
||||
|
||||
@ -14,7 +14,7 @@ This will tell you how Idris works, for using it you should read the Idris Tutor
|
||||
Idris Community* has waived all copyright and related or neighboring
|
||||
rights to Documentation for Idris.
|
||||
|
||||
More information concerning the CC0 can be found online at: http://creativecommons.org/publicdomain/zero/1.0/
|
||||
More information concerning the CC0 can be found online at: https://creativecommons.org/publicdomain/zero/1.0/
|
||||
|
||||
|
||||
.. toctree::
|
||||
|
||||
@ -9,7 +9,7 @@ Type Providers
|
||||
|
||||
Idris type providers are a way to get the type system to reflect
|
||||
observations about the world outside of Idris. Similarly to `F# type
|
||||
providers <http://msdn.microsoft.com/en-us/library/vstudio/hh156509.aspx>`__,
|
||||
providers <https://msdn.microsoft.com/en-us/library/vstudio/hh156509.aspx>`__,
|
||||
they cause effectful computations to run during type checking, returning
|
||||
information that the type checker can use when checking the rest of the
|
||||
program. While F# type providers are based on code generation, Idris
|
||||
@ -32,5 +32,5 @@ to the user.
|
||||
Example Idris type providers can be seen at `this
|
||||
repository <https://github.com/david-christiansen/idris-type-providers>`__.
|
||||
More detailed descriptions are available in David Christiansen's `WGP
|
||||
'13 paper <http://dx.doi.org/10.1145/2502488.2502495>`__ and `M.Sc.
|
||||
'13 paper <https://dx.doi.org/10.1145/2502488.2502495>`__ and `M.Sc.
|
||||
thesis <http://itu.dk/people/drc/david-christiansen-thesis.pdf>`__.
|
||||
|
||||
@ -8,7 +8,7 @@ of functions with arguments annotated as ``%static``.
|
||||
|
||||
(This is an implementation of the partial evaluator described in `this
|
||||
ICFP 2010
|
||||
paper <http://eb.host.cs.st-andrews.ac.uk/writings/icfp10.pdf>`__.
|
||||
paper <https://eb.host.cs.st-andrews.ac.uk/writings/icfp10.pdf>`__.
|
||||
Please refer to this for more precise definitions of what follows.)
|
||||
|
||||
Partial evaluation is switched off by default since Idris 1.0. It can
|
||||
@ -207,7 +207,7 @@ Specialising Interpreters
|
||||
A particularly useful situation where partial evaluation becomes
|
||||
effective is in defining an interpreter for a well-typed expression
|
||||
language, defined as follows (see the `Idris tutorial, section
|
||||
4 <http://eb.host.cs.st-andrews.ac.uk/writings/idris-tutorial.pdf>`__
|
||||
4 <https://eb.host.cs.st-andrews.ac.uk/writings/idris-tutorial.pdf>`__
|
||||
for more details on how this works):
|
||||
|
||||
::
|
||||
|
||||
@ -4,7 +4,7 @@ Type Directed Search ``:search``
|
||||
|
||||
Idris' ``:search`` command searches for terms according to their
|
||||
approximate type signature (much like
|
||||
`Hoogle <http://www.haskell.org/hoogle/>`__ for Haskell). For
|
||||
`Hoogle <https://www.haskell.org/hoogle/>`__ for Haskell). For
|
||||
example::
|
||||
|
||||
Idris> :search e -> List e -> List e
|
||||
|
||||
@ -13,7 +13,7 @@ ideally while giving up as little high level conveniences as possible.
|
||||
|
||||
They are inspired by linear types, `Uniqueness Types
|
||||
<https://en.wikipedia.org/wiki/Uniqueness_type>`__ in the `Clean
|
||||
<http://wiki.clean.cs.ru.nl/Clean>`__ programming language, and
|
||||
<https://wiki.clean.cs.ru.nl/Clean>`__ programming language, and
|
||||
ownership types and borrowed pointers in the `Rust
|
||||
<https://www.rust-lang.org/>`__ programming language.
|
||||
|
||||
|
||||
@ -14,7 +14,7 @@ the `Control.ST` library in `Idris`.
|
||||
Idris Community* has waived all copyright and related or neighbouring
|
||||
rights to Documentation for Idris.
|
||||
|
||||
More information concerning the CC0 can be found online at: http://creativecommons.org/publicdomain/zero/1.0/
|
||||
More information concerning the CC0 can be found online at: https://creativecommons.org/publicdomain/zero/1.0/
|
||||
|
||||
.. toctree::
|
||||
:maxdepth: 1
|
||||
|
||||
@ -3,7 +3,7 @@ Overview
|
||||
********
|
||||
|
||||
Pure functional languages with dependent types such as `Idris
|
||||
<http://www.idris-lang.org/>`_ support reasoning about programs directly
|
||||
<https://www.idris-lang.org/>`_ support reasoning about programs directly
|
||||
in the type system, promising that we can *know* a program will run
|
||||
correctly (i.e. according to the specification in its type) simply
|
||||
because it compiles.
|
||||
|
||||
@ -7,7 +7,7 @@ Further Reading
|
||||
Further information about Idris programming, and programming with
|
||||
dependent types in general, can be obtained from various sources:
|
||||
|
||||
- The Idris web site (http://www.idris-lang.org/) and by asking
|
||||
- The Idris web site (https://www.idris-lang.org/) and by asking
|
||||
questions on the mailing list.
|
||||
|
||||
- The IRC channel ``#idris``, on
|
||||
@ -25,7 +25,7 @@ dependent types in general, can be obtained from various sources:
|
||||
https://github.com/idris-lang/Idris-dev.
|
||||
|
||||
- Existing projects on the ``Idris Hackers`` web space:
|
||||
http://idris-hackers.github.io.
|
||||
https://idris-hackers.github.io.
|
||||
|
||||
- Various papers (e.g. [1]_, [2]_, and [3]_). Although these mostly
|
||||
describe older versions of Idris.
|
||||
@ -36,14 +36,14 @@ dependent types in general, can be obtained from various sources:
|
||||
Aspects of Declarative Languages (PADL'12), Claudio Russo and
|
||||
Neng-Fa Zhou (Eds.). Springer-Verlag, Berlin, Heidelberg,
|
||||
242-257. DOI=10.1007/978-3-642-27694-1_18
|
||||
http://dx.doi.org/10.1007/978-3-642-27694-1_18
|
||||
https://dx.doi.org/10.1007/978-3-642-27694-1_18
|
||||
|
||||
.. [2] 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
|
||||
https://doi.acm.org/10.1145/1929529.1929536
|
||||
|
||||
.. [3] Edwin C. Brady and Kevin Hammond. 2010. Scrapping your
|
||||
inefficient engine: using partial evaluation to improve
|
||||
@ -51,4 +51,4 @@ dependent types in general, can be obtained from various sources:
|
||||
15th ACM SIGPLAN international conference on Functional
|
||||
programming (ICFP '10). ACM, New York, NY, USA,
|
||||
297-308. DOI=10.1145/1863543.1863587
|
||||
http://doi.acm.org/10.1145/1863543.1863587
|
||||
https://doi.acm.org/10.1145/1863543.1863587
|
||||
|
||||
@ -15,7 +15,7 @@ existing functional programming language such as Haskell or OCaml.
|
||||
Idris Community* has waived all copyright and related or neighboring
|
||||
rights to Documentation for Idris.
|
||||
|
||||
More information concerning the CC0 can be found online at: http://creativecommons.org/publicdomain/zero/1.0/
|
||||
More information concerning the CC0 can be found online at: https://creativecommons.org/publicdomain/zero/1.0/
|
||||
|
||||
|
||||
.. toctree::
|
||||
|
||||
@ -6,7 +6,7 @@ Introduction
|
||||
|
||||
In conventional programming languages, there is a clear distinction
|
||||
between *types* and *values*. For example, in `Haskell
|
||||
<http://www.haskell.org>`_, the following are types, representing
|
||||
<https://www.haskell.org>`_, the following are types, representing
|
||||
integers, characters, lists of characters, and lists of any value
|
||||
respectively:
|
||||
|
||||
@ -49,7 +49,7 @@ Intended Audience
|
||||
|
||||
This tutorial is intended as a brief introduction to the language, and
|
||||
is aimed at readers already familiar with a functional language such
|
||||
as `Haskell <http://www.haskell.org>`_ or `OCaml <http://ocaml.org>`_.
|
||||
as `Haskell <https://www.haskell.org>`_ or `OCaml <https://ocaml.org>`_.
|
||||
In particular, a certain amount of familiarity with Haskell syntax is
|
||||
assumed, although most concepts will at least be explained
|
||||
briefly. The reader is also assumed to have some interest in using
|
||||
|
||||
@ -560,7 +560,7 @@ But what about the type of ``Type``? If we ask Idris it reports:
|
||||
Type : Type 1
|
||||
|
||||
If ``Type`` were its own type, it would lead to an inconsistency due to
|
||||
`Girard’s paradox <http://www.cs.cmu.edu/afs/cs.cmu.edu/user/kw/www/scans/girard72thesis.pdf>`_,
|
||||
`Girard’s paradox <https://www.cs.cmu.edu/afs/cs.cmu.edu/user/kw/www/scans/girard72thesis.pdf>`_,
|
||||
so internally there is a *hierarchy* of types (or *universes*):
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
@ -196,16 +196,16 @@ syntax rule, we can even go as far as:
|
||||
Aspects of Declarative Languages (PADL'12), Claudio Russo and
|
||||
Neng-Fa Zhou (Eds.). Springer-Verlag, Berlin, Heidelberg,
|
||||
242-257. DOI=10.1007/978-3-642-27694-1_18
|
||||
http://dx.doi.org/10.1007/978-3-642-27694-1_18
|
||||
https://dx.doi.org/10.1007/978-3-642-27694-1_18
|
||||
|
||||
.. [2] 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
|
||||
https://doi.acm.org/10.1145/1929529.1929536
|
||||
|
||||
.. [3] Edwin Brady and Kevin Hammond. 2010. Correct-by-Construction
|
||||
Concurrency: Using Dependent Types to Verify Implementations of
|
||||
Effectful Resource Usage Protocols. Fundam. Inf. 102, 2 (April
|
||||
2010), 145-176. http://dl.acm.org/citation.cfm?id=1883636
|
||||
2010), 145-176. https://dl.acm.org/citation.cfm?id=1883636
|
||||
|
||||
@ -4,7 +4,7 @@ License: BSD3
|
||||
License-file: LICENSE
|
||||
Author: Edwin Brady
|
||||
Maintainer: Edwin Brady <eb@cs.st-andrews.ac.uk>
|
||||
Homepage: http://www.idris-lang.org/
|
||||
Homepage: https://www.idris-lang.org/
|
||||
Bug-reports: https://github.com/idris-lang/Idris-dev/issues
|
||||
|
||||
Stability: Beta
|
||||
@ -16,7 +16,7 @@ Description: Idris is a general purpose language with full dependent types.
|
||||
meaning that some aspects of a program's behaviour can be
|
||||
specified precisely in the type. The language is closely
|
||||
related to Epigram and Agda. There is a tutorial at
|
||||
<http://www.idris-lang.org/documentation>.
|
||||
<https://www.idris-lang.org/documentation>.
|
||||
Features include:
|
||||
.
|
||||
* Full, first class, dependent types with dependent pattern matching
|
||||
|
||||
@ -26,13 +26,13 @@ infixl 9 ...
|
||||
(...) = (.) . (.)
|
||||
|
||||
||| Warbler, as named in "To Mock a Mockingbird".
|
||||
||| See http://code.jsoftware.com/wiki/Vocabulary/tilde
|
||||
||| See https://code.jsoftware.com/wiki/Vocabulary/tilde
|
||||
||| Equivalent to `join` on the Reader monad (`(->) e` in Haskell)
|
||||
reflex : (a -> a -> b) -> (a -> b)
|
||||
reflex f x = f x x
|
||||
|
||||
||| Phoenix, according to Data.Aviary.
|
||||
||| See http://code.jsoftware.com/wiki/Vocabulary/fork.
|
||||
||| See https://code.jsoftware.com/wiki/Vocabulary/fork.
|
||||
||| Equivalent to `liftA2` on the Reader monad (`(->) e` in Haskell)
|
||||
fork2 : (b -> c -> d) -> (a -> b) -> (a -> c) -> (a -> d)
|
||||
fork2 f g h x = f (g x) (h x)
|
||||
|
||||
@ -1,4 +1,4 @@
|
||||
||| The JSON language, as described at http://json.org/
|
||||
||| The JSON language, as described at https://json.org/
|
||||
module Language.JSON
|
||||
|
||||
import Language.JSON.Lexer
|
||||
|
||||
@ -80,7 +80,7 @@ foreign_prim f fname (FFun arg sc) env
|
||||
||| Idris compiler backend in use. For the default C backend, see the
|
||||
||| documentation for `FFI_C`.
|
||||
|||
|
||||
||| For more details, please consult [the Idris documentation](http://docs.idris-lang.org/en/latest/reference/ffi.html).
|
||||
||| For more details, please consult [the Idris documentation](https://idris.readthedocs.io/en/latest/reference/ffi.html).
|
||||
|||
|
||||
||| @ f an FFI descriptor, which is specific to the compiler backend.
|
||||
||| @ fname the name of the foreign function
|
||||
|
||||
@ -113,7 +113,7 @@ should not necessarily be seen as production ready nor for industrial use.
|
||||
|
||||
.SH SEE ALSO
|
||||
|
||||
+ The IDRIS web site (http://idris-lang.org/
|
||||
+ The IDRIS web site (https://idris-lang.org/
|
||||
|
||||
+ The IRC channel #idris, on chat.freenode.net
|
||||
|
||||
|
||||
@ -71,7 +71,7 @@ runArgParser = do opts <- execParser $ info parser
|
||||
PP.empty,
|
||||
PP.text "More details over Idris can be found online here:",
|
||||
PP.empty,
|
||||
PP.indent 4 (PP.text "http://www.idris-lang.org/")]
|
||||
PP.indent 4 (PP.text "https://www.idris-lang.org/")]
|
||||
|
||||
execArgParserPure :: [String] -> ParserResult [Opt]
|
||||
execArgParserPure args = preProcOpts <$> execParserPure (prefs idm) (info parser idm) args
|
||||
|
||||
@ -167,7 +167,7 @@ loadInputs inputs toline -- furthest line to read in input source files
|
||||
banner = " ____ __ _ \n" ++
|
||||
" / _/___/ /____(_)____ \n" ++
|
||||
" / // __ / ___/ / ___/ Version " ++ getIdrisVersion ++ "\n" ++
|
||||
" _/ // /_/ / / / (__ ) http://www.idris-lang.org/ \n" ++
|
||||
" _/ // /_/ / / / (__ ) https://www.idris-lang.org/ \n" ++
|
||||
" /___/\\__,_/_/ /_/____/ Type :? for help \n" ++
|
||||
"\n" ++
|
||||
"Idris is free software with ABSOLUTELY NO WARRANTY. \n" ++
|
||||
|
||||
@ -12,6 +12,6 @@ license = BSD3 but see LICENSE for more information
|
||||
brief = "This is a test package."
|
||||
readme = README.md
|
||||
version = 1234
|
||||
homepage = http://www.idris-lang.org
|
||||
sourceloc = http://ww.github.com/idris-lang/Idris-Dev
|
||||
bugtracker = http://ww.github.com/idris-lang/Idris-Dev/issues
|
||||
homepage = https://www.idris-lang.org
|
||||
sourceloc = https://www.github.com/idris-lang/Idris-Dev
|
||||
bugtracker = https://www.github.com/idris-lang/Idris-Dev/issues
|
||||
|
||||
Loading…
Reference in New Issue
Block a user