diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index f5edea6a7..6beb3e38b 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -31,7 +31,7 @@ general philosophy of the Idris project, which can be summarised as follows: properties of programs, but will not *require* them to do so Many contributions will require acccompanying tests and documentation updates. -Bug fixes in particular should be accompanied by tests, to avoid future +Bugfixes in particular should be accompanied by tests, to avoid future regressions. Library functions should be `total` as far as possible, and at least `covering` @@ -116,7 +116,7 @@ Things we probably won't accept We encourage following the camp site rule: leave the code tidier than you found it! * Primitive updates without a strong justification - - Primitives increase the burden on back end authors, for example. They may + - Primitives increase the burden on backend authors, for example. They may be necessary to support a new library, if a foreign function call is not appropriate, but we won't accept a primitive on the basis that it could be useful in future. @@ -128,9 +128,9 @@ Things we probably won't accept Idris 2 API, to minimise the maintenance burden on the compiler. * Similarly, anything which adds an external dependency. We aim to keep dependencies minimal for ease of initial installation. -* New back ends. You can implement new back ends via the Idris 2 API - and indeed - several people have. The back ends in this repository are limited to those - we are able to commit to maintaining. +* New backends. You can implement new backends via the Idris 2 API - and indeed + several people have. The backends in this repository are limited to those we + are able to commit to maintaining. Other possible contributions ---------------------------- diff --git a/README.md b/README.md index 2773fd6f2..23b461fe7 100644 --- a/README.md +++ b/README.md @@ -18,9 +18,9 @@ is often one of `scheme`, `chezscheme` or `chezscheme9.5` (depending on the version). On a modern desktop machine, this process (including tests) should take less than 5 minutes. -Idris 2 is mostly backwards compatible with Idris 1, with some minor -exceptions. The most notable user visible differences, which might cause Idris -1 programs to fail to type check, are: +Idris 2 is mostly backward compatible with Idris 1, with some minor exceptions. +The most notable user visible differences, which might cause Idris 1 programs +to fail to type check, are: + Unbound implicit arguments are always erased, so it is a type error to attempt to pattern match on one. @@ -70,8 +70,8 @@ Summary of new features: declarations. + Better type checker implementation which minimises the need for compile time evaluation. -+ New Chez Scheme based back end which both compiles and runs faster than the - default Idris 1 back end. (Also, optionally, Racket and Gambit can be used ++ New Chez Scheme based backend which both compiles and runs faster than the + default Idris 1 backend. (Also, optionally, Racket and Gambit can be used as targets). + Everything works faster :). @@ -80,9 +80,9 @@ language `TTImp`, which is essentially a desugared Idris, and is cleanly separated from the high level language which means it is potentially usable as a core language for other high level syntaxes. -Javascript +JavaScript ---------- -The javascript codegen uses the new BigInt, hence nodejs 10.4 or higher is required. +The JavaScript codegen uses the new BigInt, hence Node.js 10.4 or higher is required. Editor Plugins --------------