Abdelhakim Qbaich
281d32aeef
Complete the documentation on the Gambit backend
2020-05-03 17:37:39 -04:00
Abdelhakim Qbaich
1bbf662609
Preparation for the Gambit Scheme backend
2020-05-01 23:27:36 -04:00
Matus Tejiscak
82a23afae7
Add compatibility with the original record update syntax.
2020-04-27 18:02:25 +02:00
Edwin Brady
1262ca2fde
Merge branch 'master' into records
2020-04-27 13:36:18 +01:00
Matus Tejiscak
682ebbffb5
Wording.
2020-04-23 23:11:13 +02:00
Matus Tejiscak
d4ac7b6f52
Update typesfuns.rst.
2020-04-23 23:05:11 +02:00
Matus Tejiscak
eb5af61ebf
Add reference for the dot record syntax.
2020-04-23 21:57:03 +02:00
Jan de Muijnck-Hughes
89b68d7771
Added documentation on literate modes to the reference document.
2020-04-21 19:27:46 +01:00
Edwin Brady
9930b64c1c
Merge branch 'master' of https://github.com/jeetu7/Idris2 into jeetu7-master
2020-04-21 10:47:38 +01:00
Kamil Shakirov
dfc7001bfc
Ditto
2020-04-16 18:23:13 +06:00
Kamil Shakirov
d258584a9f
Ditto
2020-04-14 18:28:06 +06:00
Jeetu
00fc9a603d
Refactored the docs directory for latest sphinx_rtd_theme.
...
Source and build directory are seperate.
References and footnotes are named.
Other than that, tried to do no changes in the docs.
Fixed multi label in proofs-index.
Fixed most of the warnings in make html.
HTML and PDF are building.
2020-04-13 17:45:52 +05:30
Jeetu
5175743e78
Removed docs directory for adding new docs.
2020-04-13 17:41:59 +05:30
Jeetu
db25e81d48
Mostly references naming. Still footnotes are not coming on the same line as its number.
2020-04-13 16:40:23 +05:30
Jeetu
a24511eae2
Spelling mistake corrected.
2020-04-10 16:14:54 +05:30
Jeetu
a9ac084b8c
Added instruction for virtual environment for python.
2020-04-10 13:34:03 +05:30
Kamil Shakirov
0ea595817a
Fix some typos in the tutorial
2020-04-09 13:48:12 +06:00
Edwin Brady
e383c2793d
Merge pull request #265 from then0rTh/patch-1
...
fix typo in docs/tutorial/typesfuns.rst
2020-04-06 22:02:40 +01:00
then0rTh
e6fe418a6b
fix typo in docs/tutorial/typesfuns.rst
...
duplicated word
2020-04-04 22:58:34 +02:00
Kamil Shakirov
55b3f880d3
Update Idris prompt in the tutorial
2020-04-03 16:44:12 +06:00
Guillaume Allais
2c7b2469a4
[ cosmetic ] cleanup trailing whitespace + typos
2020-04-01 10:19:27 +01:00
Edwin Brady
e027e0c434
--build and --clean now looks at executable field
...
Executables now get built and deleted. Install doesn't do anything with
the executable, and --clean only deletes the executable itself (not any
support files or libraries that might also have been generated in the
exec directory)
2020-03-31 22:33:58 +01:00
Edwin Brady
b3dc643029
Better disambiguation of pairs
...
The names weren't fully explicit in the elaborator, so ambiguity
resolution wasn't able to take advantage of type-directed pruning. Now
they're explicit (but hard-coded, which we should fix later...) so they
can be resolved more easily.
2020-03-31 18:12:34 +01:00
Edwin Brady
736699c729
Better ambiguity resolution
...
Do two passes through delayed elaborators (it's impossible to predict
dependency order). Possibly this should keep going as long as it's
making progress? I'll consider that later.
2020-03-31 13:04:42 +01:00
Edwin Brady
95a90d0a05
Note on %hint in documentation
2020-03-29 13:02:10 +01:00
Edwin Brady
41ec1fc587
Minor documentation edits
2020-03-28 16:00:33 +00:00
Edwin Brady
52273bec5d
Some documentation edits
...
Update Getting Started with installation instructions
2020-03-28 14:21:12 +00:00
Edwin Brady
2938e86421
Ints in buffers are 32 bit
...
...for consistency with Idris 1 (probably to be revisited later). So,
when working via the scheme primitives, we need to read/write 32 bits.
2020-03-27 20:54:39 +00:00
Edwin Brady
ebafddcfc9
Look for scrutinee type in case
...
We can work out what it should be since each case is supposed to have
the same type, so we can look ahead to the alternatives. This way, we
don't have to rely on the scrutinee alone to calculate the type of the
case block. (Idris 1 does this too but I've only just encountered the
need for it in Idris 2 now!)
2020-03-27 14:27:33 +00:00
Edwin Brady
776abebba1
Merge pull request #227 from ska80/typedd-book/chapter13-14
...
Port code examples for chapters 13 and 14 from TypeDD book
2020-03-18 20:37:26 +00:00
Kamil Shakirov
1704495f06
Port code examples for chapters 13 and 14 from TypeDD book
2020-03-13 09:50:22 +06:00
Matthew Wilson
6c11d7a162
various copyedits
2020-03-07 23:18:49 -05:00
Edwin Brady
1dd81ff10b
Look under . for function name on lhs
...
Need this to rule out some ambiguous names. Fixes #204 .
2020-03-05 11:22:48 +00:00
Edwin Brady
0e98f6383f
Small fixes in readline ffi tutorial
2020-03-03 23:35:19 +00:00
Edwin Brady
1616879c3e
Some FFI documentation
...
Explaining how to write the most basic Idris bindings for readline,
taking account of how to allocate Strings in the completion callback.
Also adds the basic API as a sample, which can be used as a starting
point for other packages containing C bindings.
2020-03-03 23:23:49 +00:00
Edwin Brady
10c70711f4
Initial documentation of back ends
2020-03-03 19:33:37 +00:00
Edwin Brady
6023889115
Note on String in FFI docs
2020-03-03 17:39:13 +00:00
Edwin Brady
526c5f7d3a
Add missing bit of example in ffi docs
2020-03-02 15:30:50 +00:00
Edwin Brady
21a7b46ca1
More FFI doc typos
2020-03-02 14:54:27 +00:00
Edwin Brady
ea7e8c38f6
Fix ffi text
2020-03-02 14:49:28 +00:00
Edwin Brady
2893e6f9e8
Initial FFI documentation
2020-03-02 14:29:26 +00:00
Edwin Brady
a5c356f998
Basic support for struct in FFI
...
Just in the Chez backend for now, and not allowing strings or functions
due to limitations of Chez.
2020-03-01 23:23:21 +00:00
Edwin Brady
052c98d86e
Merge pull request #202 from glmxndr/patch-1
...
Dependent record example "length" field naming
2020-02-28 00:15:52 +00:00
Edwin Brady
b83f01e2f4
Small documentation updates
2020-02-28 00:15:03 +00:00
GhiOm
37af02eb2a
Update updates.rst
2020-02-27 12:51:11 +01:00
Edwin Brady
d67dcd6758
Minor documentation edits
2020-02-26 22:37:26 +00:00
Edwin Brady
f08eb3d6ce
TypeDD notes moved to docs/
2020-02-26 21:53:45 +00:00
Edwin Brady
99a133c582
Document changes since Idris 1 in more detail
2020-02-26 21:46:03 +00:00
Edwin Brady
e340747b1f
Some documentation on changes since Idris 1
2020-02-26 20:19:54 +00:00
Edwin Brady
1bb028ae47
Update proof tutorial for Idris 2
2020-02-26 12:33:01 +00:00
