idris-lang/Idris-dev
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris-dev.git synced 2024-10-04 09:58:27 +03:00
Code Issues Projects Releases Wiki Activity

Updated wording in CONTRIBUTING.md

Browse Source
This commit is contained in:
Jan de Muijnck-Hughes 2015-03-24 07:46:01 +00:00
parent fe3d1f7c79
commit 4a1fcdd7ae
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
CONTRIBUTING.md
View File

@ -37,14 +37,14 @@ Idris ships with a set of packages in `libs/` that is provided as a default libr
These packages should not be seen as the *standard* as when working with dependent types we do not necessarily know how best to work with dependent types.
These packages offer functionality that can be built on top of when constructing Idris programs.
One major point to make is that everything in prelude will be imported automatically, unless given the `--noprelude` option.
When working with packages in `libs/`, it is important to realise that everything in prelude will be imported automatically, unless given the `--noprelude` option.
Likewise, the contents of base are available with no special options.
The other two packages that ship with Idris, contrib and effects, require the use of the `-p` command-line argument to bring their contents into the include path.
New contributions should probably be sent to contrib first, so that they can get maintained with the Idris distribution.
If they turn out to be widely applicable and useful, they may later be moved into base.
As Idris is still being developed we are open to suggestions and changes that make improvements to these default packages.
Major changes to the library (or Idris itself) should ideally be discussed first through the projects official channels of communication:
Major changes to the library (or Idris itself) should ideally be discussed first through the project's official channels of communication:
1. The mailing List.
1. On our IRC Channel `#idris` on freenode, or