idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-01 01:09:03 +03:00
Code Issues Projects Releases Wiki Activity
3,318 Commits 5 Branches 9 Tags 101 MiB
b7bda5e96d
Commit Graph

49 Commits

Author SHA1 Message Date
Denis Buzdalov
b7bda5e96d [ docs ] Fix the formatting warning in the docs 2023-08-01 12:48:33 +01:00
CodingCellist
51403ab18c
[ fix ] Only set IDRIS2_PREFIX if it is unset (fixes Issue 3022) (#3024) 2023-07-31 08:18:15 +01:00
Andre Videla
9797a79b53 [ new ] Allow fixities to be hidden with %hide 
* Change the printing of namespaced operator to show
  parenthesis around operators
* Update warning when conflicting fixities are found
* Do not warn about redundant but compatible fixities
 2023-06-14 11:19:59 +01:00
Walter Smuts
ab2d828887 Typos: Run 'typos -w' command over docs/ 
Only running over "docs/" directory since it will likely have the
largest postivie impact and cause fewest issues.

Typos will do simple find-and-replace when it detects a word not in it's
dictionary. It does not have any regard for formatting based on
surrounding context. Care must be taken not no merge variable names in
same scope etc.

Typos can be driven by Github Actions:
https://github.com/crate-ci/typos/blob/master/docs/github-action.md

Tool: https://github.com/crate-ci/typos
 2023-06-08 13:41:54 +02:00
Mathew Polzin
63a22b819d
[docs] javascript FFIs and packaging of JS or C support files (#2842) 
* Add documentation on javascript FFIs and packaging of JS or C support files.

* Add to changelog.

* line length

* add some detail about the install directories for packages.
 2023-01-07 21:40:47 +00:00
Denis Buzdalov
2dfd7e5259 [ doc ] Minor syntactic correction in the code example 2022-12-20 16:36:27 +00:00
Zoe Stafford
0010768ee7
[doc] Rewrite docs for %builtin and nat optimisations (#2426) 2022-04-22 14:52:02 +01:00
Denis Buzdalov
9d93e74012 [ doc ] Fix prefix var, IDRIS2_PREFIX is used, not PREFIX 2022-03-10 14:25:16 +00:00
Mathew Polzin
e7ed760016
[ new ] optional language version field to ipkg files. (#2256) 2022-01-20 10:05:53 +00:00
teggot
d3aed0404c
[ fix #1959 ] use modern record update syntax (#2196) 2021-12-16 18:23:18 +00:00
Mathew Polzin
0eba4c691e
Add %deprecate pragma (#2086) 2021-11-17 10:41:03 +00:00
Kamil Shakirov
ae411fe756 [ doc ] Mark code blocks as Idris code 2021-11-11 18:55:11 +00:00
André Videla
e4d566b28c
Update documentation and changelog for string interpolation (#2013) 
* Update documentation and changelog for string interpolation

* Fix typo in changelog

* fix documentation about desugaring of interpolate

* Update CHANGELOG.md

Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>

Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>
 2021-10-18 11:45:32 +01:00
André Videla
274954998b
Implement generic interpolation (#1967) 
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
 2021-10-13 17:26:54 +01:00
Guillaume ANDRIEU
71511f4bdd
code-blocks missing in the docs (#1911) 
* Update strings.rst

For some reasons the code blocks which are not set as 'idris' are not displayed in the readthedocs rendering.

* Update overloadedlit.rst

* Update overloadedlit.rst
 2021-09-08 18:46:46 +01:00
Peter Hajdu
2d7ddc6e64 [ fix #472 ] Port doc about comments from Idris1 2021-08-27 14:58:35 +01:00
Denis Buzdalov
377b21e376 [ doc ] Remove trailing spaces from doc files 2021-08-11 12:50:02 +01:00
André Videla
440a3affd5
Update docs/source/reference/strings.rst 
Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>
 2021-07-19 10:37:22 +00:00
André Videla
396ebe2023 Add documentation for new string literals 2021-07-18 22:32:26 +00:00
André Videla
9aa7a4303a Added documentation for new string literals 2021-07-18 21:37:20 +00:00
Edwin Brady
980b6174ec Added --mkdoc to CHANGELOG too 2021-06-23 18:31:31 +01:00
Edwin Brady
80aeecaac0 Add note on --mkdocs 2021-06-23 18:29:49 +01:00
Jan de Muijnck-Hughes
692054516e
A rough dump of how to debug idris2's workings. (#1464) 2021-05-26 10:19:40 +01:00
Zoe Stafford
7fe8c42116
[ builtin ] O(1) integerToNat for any 'Nat'-like type (#1403) 2021-05-13 18:44:24 +01:00
Zoe Stafford
8a7aeca1b0
[ builtin ] O(1) natToInteger for any 'Nat'-like type (#1363) 2021-05-10 12:14:19 +01:00
Zoe Stafford
c75b3f7f14
Add Agda-like builtins (#1253) 
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
 2021-04-22 13:08:32 +01:00
Denis Buzdalov
a74d8e6c2d [ doc ] Documentation of package lookup was clarified a bit. 2021-03-04 14:51:57 +00:00
Denis Buzdalov
ae43ff688c [ doc ] Orphaned todo block was removed 2021-03-01 14:50:31 +00:00
Edwin Brady
03b8198560 Add environment variables to documentation 2021-02-28 14:18:19 +00:00
Edwin Brady
d617290dd5 Update packaging documentation 2021-02-27 18:20:55 +00:00
Jan de Muijnck-Hughes
3a6e779acf Extended Literate support to include LaTeX. 2020-12-07 14:54:35 +00:00
Jan de Muijnck-Hughes
9c5198cde3 Fixed docs and improved Literate mode. 
+ Expanded the documentation on how to use literate modes.
+ Added invisible code blocks in Markdown using specially tagged comment blocks: `<!-- idris -->`.
+ Fixed OrgMode specificaton to recognise comment blocks properly.
 2020-12-07 14:54:35 +00:00
Matus Tejiscak
d98686d4f8 Update doc, fix tests. 2020-09-10 20:33:08 +02:00
Matus Tejiscak
e491e2969e Re-introduce %prefix_record_projections. 2020-09-10 20:18:51 +02:00
Matus Tejiscak
aebe3c19d9 Revert postfix dotted application. 2020-09-10 19:00:48 +02:00
stasoid
a70446c8ff
Clarify what 'invisible' code means in literate.rst (#615) 
Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>
Co-authored-by: stasoid <x@x.x>
 2020-08-31 18:37:48 +01:00
Giuseppe Lomurno
627d340b62 Docs for overloaded literals 2020-08-05 11:51:27 +02:00
Matus Tejiscak
168e5d8a21 Update postfix projection doc. 2020-07-07 21:06:35 +01:00
Matus Tejiscak
98e94f956e Rename record projections to postfix projections. 2020-07-07 21:06:35 +01:00
Matus Tejiscak
4af4ae01ae Update the postfix projection doc. 2020-07-07 21:06:35 +01:00
Matus Tejiscak
a4c59204c5 Add postfix projection sections. 2020-07-07 21:06:35 +01:00
Matus Tejiscak
bfb56ae71a Update the doc. 2020-07-07 21:06:35 +01:00
Matus Tejiscak
b46064f688 Update docs and tests. 2020-07-07 21:06:35 +01:00
Christian Rasmussen
3bf384860a Add documentation for sourcedir/builddir/outputdir 2020-06-28 19:56:02 +02:00
Mark Barbone
59dceb857f Make reference and source agree about literate markdown 2020-06-19 10:08:47 +01:00
Edwin Brady
508b136866
Merge branch 'master' into add-warnings-to-rtd 2020-05-25 00:38:22 +01:00
Fabián Heredia Montiel
731a416043 Split Package Specific Lexer/Rules from Lexer/{Common,Source} and Refactor Idris/Package 
Co-authored-by: Matus Tejiscak <ziman@functor.sk>
 2020-05-24 16:01:17 -05:00
Jan de Muijnck-Hughes
43c5075f6e Use reST directives to make warnings and TODOs explicit in the documentation. 2020-05-23 19:57:50 +01:00
Edwin Brady
fd55e629ee Copy more files over from Idris2 2020-05-20 11:23:04 +01:00