André Videla
4bca967121
Merge pull request #2352 from tasuki/fix-wiki-links
...
[doc] Fix wiki links
2022-03-14 18:29:06 +00:00
Vit Brunner
b1040a26b3
Appease the linter
...
Hey I haven't even touched those things!
2022-03-14 18:13:57 +01:00
Vit Brunner
f16b5d63d2
Fix link syntax in CONTRIBUTING.md
2022-03-11 20:33:31 +01:00
Vit Brunner
3d7b946fb9
Fix links to GitHub wiki
2022-03-11 20:31:43 +01:00
Denis Buzdalov
05d64483f6
[ refactor ] Factor out a type for primitive types out of Constant
2022-03-10 23:07:20 +00:00
Denis Buzdalov
9d93e74012
[ doc ] Fix prefix var, IDRIS2_PREFIX is used, not PREFIX
2022-03-10 14:25:16 +00:00
Guillaume Allais
14f2196d15
[ doc ] return module header docs
2022-03-09 13:31:30 +00:00
stefan-hoeck
51eb854a60
[ fix ] euclidian mod and div for scheme backends
2022-03-08 17:40:29 +00:00
stefan-hoeck
405f80946b
[ fix ] euclidian div and mod for JS backend
2022-03-08 17:40:29 +00:00
G. Allais
fd02bf8b3e
[ fix #2303 ] remove quadratic unwords ( #2345 )
2022-03-07 18:34:06 +00:00
Guillaume Allais
b87d7e3b62
[ perf ] do not public export FromString
2022-03-07 15:39:27 +00:00
Sage Hane
c2718684d8
[ doc ] add missing backquote
2022-03-07 12:48:04 +00:00
G. Allais
1c396744d9
[ doc ] :printdef for interface implementations ( #2340 )
2022-03-07 11:47:20 +00:00
Robert Wright
6b367010ce
Inline SnocList foldl utility function
...
The scoping of the utility function meant that Idris treats `foldl f z (xs :< x)` and `f (foldl f z xs) x` as two different terms, making proving things about it difficult.
2022-03-07 11:46:43 +00:00
Joel Berkeley
0ab0ecb199
add replaceAt for List ( #2335 )
2022-03-03 23:40:18 +00:00
Joel Berkeley
f436388a6b
adopt backend implementations of pow ( #2334 )
2022-03-03 23:39:25 +00:00
Joel Berkeley
f317555967
[ ci ] install mingw64 gcc for windows ( #2338 )
...
Co-authored-by: Ben Hormann <benhormann@users.noreply.github.com>
2022-03-03 22:29:25 +00:00
G. Allais
1011cc6162
[ papers ] Tychonoff (Part I) ( #2332 )
2022-02-24 11:12:53 +00:00
Tim Engler
8ffad8878f
Fixes problem where when compiling using "load-file" in ide mode causes compilation to run slower and slower each time. ( #2136 )
2022-02-21 12:11:37 +00:00
Jan de Muijnck-Hughes
4ba3bb6670
[ fix ] Literate things ( #2312 )
...
Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>
2022-02-18 11:29:52 +00:00
Guillaume Allais
c8a5ad6d97
[ doc ] REPL's :doc should support brackets too
2022-02-17 20:19:36 +00:00
octeep
768d164ec9
[ network ] add binary support for socket + fix recvAll ( #2308 )
2022-02-16 20:12:24 +00:00
Balazs Komuves
3345460fe9
[ fix #2176 ] Records in where-blocks are in the wrong namespace ( #2187 )
2022-02-16 15:43:50 +00:00
Denis Buzdalov
b727ae4a97
[ new ] Add a Monoid instance of the f a where f is Applicative
2022-02-16 14:23:56 +00:00
Denis Buzdalov
e2487106fd
[ prelude ] Ease Compose compositions ( #2324 )
2022-02-16 14:19:25 +00:00
Marcus Granado
fbfde5f770
B is defined as proposition y=z
2022-02-15 14:17:01 +00:00
Denis Buzdalov
80ff76b357
[ cleanup ] Remove unused get's, replace get+put with update ( #2310 )
...
Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>
2022-02-12 10:39:53 +00:00
CodingCellist
c5d96a10e7
[ base ] Split a list according to a decidable property ( #2302 )
2022-02-11 11:21:20 +00:00
Joel Berkeley
5abc01453d
add deleteAt for List ( #2317 )
2022-02-11 09:28:36 +00:00
G. Allais
33d99adb53
[ linear ] These seem useful ( #2316 )
2022-02-11 09:28:15 +00:00
Guillaume Allais
bec4a0a88e
[ re #499 ] quantity-aware with-clauses
2022-02-09 09:19:40 +00:00
Guillaume Allais
6f509df268
[ debug ] logging for dotting decision
2022-02-09 09:19:40 +00:00
Sören Tempel
ae04a54c37
[ fix ] Flush standard when prompting for package information
...
On Unix-like operating systems stdio.h is usually line-buffered. As
putStr uses fputs(3) from stdio.h internally, output will be written to
standard out after a newline character is written to the buffer. Since
the various prompts written by `idris2 --init` don't contain a newline
character they are buffered indefinitely. As such, the prompt strings
themselves are never presented to the user.
To fix this issue, this commit introduces a prompt utility procedure
which prints a prompt string and afterwards flushes standard output
before receiving input using getLine. This ensures that the prompt
string is always written before input is retrieved via getLine.
This is similar to c725b11c89
2022-02-08 15:35:44 +00:00
Mathew Polzin
8208ed2590
[ new ] A couple of nearly trivial proofs about list length. ( #2311 )
2022-02-07 17:51:04 +00:00
Nick Drozd
2c9bf24d2f
[ libs ] Strengthen some totality checks ( #2304 )
2022-02-03 18:41:51 +00:00
Robert Wright
1776efa8a5
Allow Type-level String operations
2022-02-03 16:10:47 +00:00
CodingCellist
ad3a1c153c
Document Test.Golden change in CHANGELOG.md ( #2301 )
2022-02-02 11:36:28 +00:00
CodingCellist
f4b78157cc
[ base,tests ] Reduce dependency on contrib ( #1595 )
2022-02-02 11:17:10 +00:00
Guillaume Allais
56009ad3ac
[ cleanup ] silence warnings in libs
2022-02-02 11:09:03 +00:00
madman-bob
0ee9632e45
[ refactor ] Abstract Prelude.elem to work with all Foldables ( #2294 )
2022-02-01 21:34:29 +00:00
Denis Buzdalov
b17e65fc82
[ base ] Generalise existing min-max semigroups and add monoid for Fin ( #2298 )
2022-02-01 21:24:49 +00:00
André Videla
208adb7202
[ linear ] add utilities for linear datastructures ( #2293 )
2022-02-01 21:22:16 +00:00
Trevor Arjeski
a2c7e9f306
Update TypeDD Chapter 11 for idris2 ( #2296 )
2022-01-30 20:49:26 -08:00
Stefan Höck
44245e1683
[ fix ] issue #2288 ( #2289 )
2022-01-28 09:01:09 +00:00
Guillaume Allais
3c63902d82
[ new ] Dependent Tagless Final
2022-01-27 17:26:52 +00:00
Michael Messer
26527c3a6e
[ fix ] expose Data.Seq.Internal ( #2291 )
2022-01-26 18:38:22 +00:00
Alias Qli
1ba0008486
[contrib] A finger tree implementation ( #1454 )
2022-01-25 18:29:48 +00:00
octeep
9a9412e1a2
make writeBufferData return the number of bytes that have been written ( #2276 )
2022-01-25 13:25:06 +00:00
teggot
c47b392d08
[ fix #2208 ] Add interactive commands to help message ( #2209 )
2022-01-25 12:38:49 +00:00
G. Allais
ec5afa5065
[ libs ] move propaganda out of contrib ( #2213 )
2022-01-25 12:25:55 +00:00
