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
