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
teggot
d3aed0404c
[ fix #1959 ] use modern record update syntax ( #2196 )
2021-12-16 18:23:18 +00:00
Denis Buzdalov
2a4197e909
[ doc ] Some documentation on := syntax of let bindings ( #1487 )
...
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
2021-06-03 16:49:31 +01:00
Georgi Lyubenov
0bbc3cf42b
Update section on custom code gens in updates.rst
...
It is now possible to write your own code generation.
2021-04-07 16:28:46 +01:00
Denis Buzdalov
a74d8e6c2d
[ doc ] Documentation of package lookup was clarified a bit.
2021-03-04 14:51:57 +00:00
Dong Tsing-hsuen
505224e9fc
[ typo ] Enum -> Range ( #1099 )
2021-02-22 10:05:08 +00:00
Denis Buzdalov
a1b624a3bc
Tiny fix of the formatting in the recently added documentation.
2020-12-08 08:56:38 +00:00
Ruslan Feizerahmanov
1dba32a0c4
[ doc ] new application syntax ( #820 )
2020-12-07 18:59:49 +00:00
Fangyi Zhou
df4c454f4e
Typo in updates.rst
2020-08-17 19:33:14 +01:00
elsanussi-s-mneina
19bced702d
fix typo: "lowercase later" to "lowercase letter"
...
I think this is a spelling mistake.
2020-07-15 09:50:19 -04:00
Keller, Bryn
a5449d926e
Update docs to reflect changes to ipkg format
2020-06-05 22:14:16 -07:00
Boyd Stephen Smith Jr
38876800ca
Mention %access specifically
...
(The first failure I got when trying to compile Idris 1.3.1 code with
Idris2.)
2020-05-27 12:51:41 -05:00
Edwin Brady
9c5594223e
Small documentation updates
2020-05-25 01:02:07 +01:00
Edwin Brady
498421a236
All functions now need to be covering by default
...
This has caught a couple of things in the Idris 2 code base itself. Some
tests needed partial annotations too.
2020-05-24 19:58:20 +01:00
Edwin Brady
fd55e629ee
Copy more files over from Idris2
2020-05-20 11:23:04 +01:00
