idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-21 10:41:59 +03:00
Code Issues Projects Releases Wiki Activity
2,830 Commits 6 Branches 9 Tags 115 MiB
e3f31d3542
Commit Graph

66 Commits

Author SHA1 Message Date
KDr2
e3f31d3542 fix a case typo in document 2022-05-10 08:27:24 +01:00
Denis Buzdalov
9d93e74012 [ doc ] Fix prefix var, IDRIS2_PREFIX is used, not PREFIX 2022-03-10 14:25:16 +00:00
teggot
d3aed0404c
[ fix #1959 ] use modern record update syntax (#2196) 2021-12-16 18:23:18 +00:00
Denis Buzdalov
a4eb8b2ec3 [ doc ] Fix a complain of not being in a toctree 2021-11-17 10:50:49 +00:00
G. Allais
96c44abb64
[ new ] :doc for keywords (#2028) 
* [ new ] :doc for keywords

* [ doc ] for visibility

* [ more ] fixing help text, sentence for "mutual"

* [ doc ] for if then else

* [ doc ] for implicit arguments

* [ doc ] import

* [ cleanup ] doc for data

* [ doc ] for record

* [ doc ] for forall quantifier

* [ doc ] for `in' keyword

* [ doc ] for parameters block

* [ fix ] missing fence

* [ doc ] for where and mutual blocks

* [ doc ] for namespace blocks

* [ doc ] for with/proof

* [ doc ] for do blocks

* [ doc ] for rewrite

* [ doc ] for let binding

* [ doc ] for case...of and interfaces

* [ doc ] for fixity
 2021-10-26 18:58:06 +01:00
Guillaume ALLAIS
a7d73d0d3d [ new ] ellipses for with patterns 
Rather than Agda's `...` we use the common symbol for "I don't care": `_`.
 2021-08-31 22:50:46 +01:00
Denis Buzdalov
377b21e376 [ doc ] Remove trailing spaces from doc files 2021-08-11 12:50:02 +01:00
Denis Buzdalov
150bffc307 [ doc ] Hopefully fix the linting problem in the docs 2021-08-10 15:11:32 +03:00
Mathew Polzin
b03395debe
Merge pull request #1603 from ska80/remove-realpath-notes 
Remove all mentions of `realpath` from docs
 2021-07-26 12:38:39 -07:00
Niklas Larsson
4b0edbaa4f Update windows docs with gotchas 2021-07-23 15:48:54 +02:00
Niklas Larsson
603c60efec Add some docs about building on Windows 2021-07-23 10:58:38 +01:00
Ellis Kesterton
e5879dc687 Document --init 
Reference the --init option for creating package files in the tutorial documentation.
 2021-07-22 19:15:33 +01:00
Edwin Brady
877e830133 A couple of documentation corrections 
A CHANGELOG update, and a correction on data type names which has been
wrong in the crash course for some time now!
 2021-07-17 14:20:32 +01:00
Kamil Shakirov
c4b41ee1ff Remove all mentions of realpath from docs 
`realpath` is no longer needed to run executables.
 2021-07-16 21:20:11 +06:00
Edwin Brady
3c88c33f15
Merge pull request #1452 from nickdrozd/emacs-doc 
Update Emacs idris-mode doc
 2021-07-15 23:38:26 +01:00
Kamiλ Shakirov
8e30b296c0
[ refactor ] Remove Data.Strings module (#1607) 2021-06-28 13:48:37 +01:00
Alissa Tung
41c3fd2632
[docs] ind-ind ind-rec rec-rec in style of fwddecl (#1558) 
Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>
 2021-06-16 16:20:11 +01: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
Kamiλ Shakirov
ad656a8d47
Remove realpath (#1457) 2021-05-25 11:01:28 +01:00
Nick Drozd
dc5c3963e4 Update Emacs idris-mode doc 2021-05-22 16:19:17 -05:00
Ohad Kammar
618c71477e
[ close #1384 ] built-in Snoc-lists [< 1, 2, 3 ] (#1383) 2021-05-20 12:56:25 +01:00
Ruslan Feizerakhmanov
51184c156d [doc] Interface constructors 2021-05-08 11:36:12 +03:00
Raoul Hidalgo Charman
2c8f2483de Update docs to reflect usage of >> in do syntax 2021-05-01 15:18:49 +01:00
Nil Geisweiller
bb25050746 Remove redundant to 2021-02-18 09:56:42 +00:00
Nil Geisweiller
f390fba766 Rename Sotrable to Storable 2021-02-16 09:51:44 +00:00
Guillaume ALLAIS
5aa4262792 [ fix ] some of the docs 2021-02-10 00:37:06 +00:00
Denis Buzdalov
052e3f0908 A tiny doc fix: heading line was not long enough. 2021-02-04 16:48:19 +00:00
Nil Geisweiller
0a24821429 Fix documentation link in typesfuns tutorial 2021-02-02 11:04:44 +00:00
stefan-hoeck
29a6aa45e0 fixed whitespace for *.md and .rst files 2021-01-22 15:08:49 +00:00
Jonathan Lorimer
4bc1d17506 add command history faq 2020-12-29 16:52:04 -05:00
Jonathan Lorimer
47df67af16 add rlwrap docs 2020-12-29 14:55:00 -05:00
G. Allais
3f6b99e979
[ fix #657 ] RigCount for interface parameters (#808) 2020-12-11 11:58:26 +00:00
DavidTheBugWriter
b4b800e967 Update starting.rst 
Hellow world execute fails on Macos as it doesn't have realpath by default & one needs to install it with coreutils first.
 2020-10-24 12:35:13 +01:00
Matus Tejiscak
668762e693 Merge branch 'revert-projections' into master 2020-10-11 08:12:00 +02:00
Brandon Elam Barker
28cf2a3083 Making "functional dependencies" easier to find 2020-09-30 19:33:02 +01: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
Matus Tejiscak
3b6d7a22e3 Remove forgotten .field from docs. 2020-07-07 21:06:35 +01:00
Matus Tejiscak
b46064f688 Update docs and tests. 2020-07-07 21:06:35 +01:00
Tim Engler
14725dac67 Describe what is meant by "use" 
I hit a roadblock trying to understand linear types, because I couldn't figure out what is meant to "use" a variable. I eventually think I figured it out, by reading "Linear types can change the world!", but it was not easy to do so. I think a better description of what "use" means would be very helpful for those unfamiliar with linear types, so I took a stab at it. Hope it helps.
 2020-07-06 12:38:03 +01:00
Denis Buzdalov
066b37feb4 Tiny doc fix about combination of import public and import .. as. 2020-07-06 11:23:56 +01:00
Edwin Brady
4c5d26f050 Add note on import...as to tutorial 2020-07-04 23:30:13 +01:00
Edwin Brady
950431a9ce Note in tutorial on qualified do 2020-07-04 23:12:03 +01:00
Kamil Shakirov
f094a52ba9 Update docs 2020-06-30 18:44:36 +06:00
Dario Vladovic
9cc1215f6c Format Homebrew install code block 2020-06-22 17:17:11 +01:00
Edwin Brady
1e6314c4cc
Merge pull request #345 from edwinb/hasio 
HasIO interface for IO actions
 2020-06-21 20:24:29 +01:00
TomasPuverle
833a24cb45
Updated documentation for export (#344) 
Co-authored-by: Thomas Herzog <thomas-github@poto.cafe>
 2020-06-21 20:17:34 +01:00
Edwin Brady
dbdf7dab3d Back to HasIO, remove MonadIO 
Following a fairly detailed discussion on slack, the feeling is
generally that it's better to have a single interface. While precision
is nice, it doesn't appear to buy us anything here. If that turns out to
be wrong, or limiting somehow, we can revisit it later. Also:

- it's easier for backend authors if the type of IO operations is
  slightly less restrictive. For example, if it's in HasIO, that limits
  alternative implementations, which might be awkward for some
  alternative back ends.
- it's one less extra detail to learn. This is minor, but there needs to
  be a clear advantage if there's more detail to learn.
- It is difficult to think of an underlying type that can't have a Monad
  instance (I have personally never encountered one - if they turns out
  to exist, again, we can revisit!)
 2020-06-21 19:21:22 +01:00
Edwin Brady
1b15463746 Update libraries and docs with HasIO/MonadIO 2020-06-21 15:25:40 +01:00
Dario Vladovic
cc61d4d3d8
Add Homebrew installation instructions 2020-06-21 13:37:36 +02:00