Commit Graph

72 Commits

Author SHA1 Message Date
Steve Dunham
9e84b153bd
Add %foreign_impl pragma for augmenting ffi functions (#3303)
* Add %foreign_impl pragma for augmenting ffi functions

* document how conflicting %foreign_impl are handled
2024-06-11 17:45:09 +01:00
Jorge Gomez
0742b3ba97 [ doc ] reference intro info on elab 2024-06-05 07:53:48 +01:00
Jorge Gomez
d7d84868a5 fix: typos in "Expressions" 2024-06-04 13:08:00 +01:00
Steve Dunham
388fe83bdc
[ doc ] document %cg pragma (#3217)
* [ doc ] document %cg pragma

* [ doc ] add more detail to %cg documentation
2024-03-17 10:40:07 +00:00
André Videla
7c70762f25 fix typos 2024-02-24 12:36:44 +00:00
André Videla
2859fcee08 Update docs/source/reference/operators.rst 2024-02-24 12:36:44 +00:00
André Videla
93de3e0e07 Update docs/source/reference/operators.rst 2024-02-24 12:36:44 +00:00
André Videla
e7a4914f11 Update docs/source/reference/operators.rst 2024-02-24 12:36:44 +00:00
André Videla
e1f4fbba83 Update docs/source/reference/operators.rst 2024-02-24 12:36:44 +00:00
André Videla
23b2ddd179 Update docs/source/reference/operators.rst 2024-02-24 12:36:44 +00:00
André Videla
b22c7f8289 Update docs/source/reference/operators.rst 2024-02-24 12:36:44 +00:00
André Videla
ef0ca76b4c Update docs/source/reference/operators.rst 2024-02-24 12:36:44 +00:00
André Videla
c4c79c9115 Update docs/source/reference/operators.rst 2024-02-24 12:36:44 +00:00
André Videla
bcb225568a Update docs/source/reference/operators.rst 2024-02-24 12:36:44 +00:00
André Videla
c6fbd27c6c Update docs/source/reference/operators.rst 2024-02-24 12:36:44 +00:00
André Videla
eb9d4d65a5 fix typo in doc 2024-02-24 12:28:10 +00:00
Andre Videla
c3651509e0 add operator documentation 2024-02-24 12:28:10 +00:00
Andre Videla
3d2c854257 update docs 2024-02-24 12:28:10 +00:00
Adam Brouwers-Harries
ecfe1bde70 use in cccompilerTest, correctly set DYLD_LIBRARY_PATH, use idrisGetEnv in CC.idr and update envvars documentation 2023-12-13 15:21:41 +00:00
Steve Dunham
60ec783483 [ doc ] updates to hint documentation. 2023-11-23 14:28:15 -08:00
Steve Dunham
a03c3bf376 [ doc ] Add missing pragmas to documentation 2023-11-22 09:13:42 -08:00
Thomas E. Hansen
db87cef0ad [ doc ] Headings for envvars based on use-time
Some envvars are only used at build-time, some only at runtime, and lots
are used at both. This clearly cagetorises them accordingly in the docs.
2023-11-01 09:41:22 +00:00
CodingCellist
fcecb165b9
[ doc ] Document failing blocks (#3114) 2023-10-23 11:40:18 +01:00
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