Commit Graph

862 Commits

Author SHA1 Message Date
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
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
G. Allais
ec5afa5065
[ libs ] move propaganda out of contrib (#2213) 2022-01-25 12:25:55 +00:00
James Cook
e82600c4d6
[ opt ] transform rule making List.length tail-recursive. (#2100) 2022-01-24 16:12:29 +00:00
stefan-hoeck
1b3be25075 [ breaking, totality ] fGetLine should be covering 2022-01-20 17:48:11 +00:00
Zoe Stafford
5e42bbfcc9
Merge pull request #2274 from octeep/main
make readBufferData return the number of bytes that have been read
2022-01-20 13:11:13 +00:00
Robert Wright
d85016b64d Add Fin modular arithmetic Num instance 2022-01-20 10:13:20 +00:00
Stefan Höck
ca5b1ba094
[ totality ] Data.String.words should be total (#2262) 2022-01-20 09:58:50 +00:00
MarcelineVQ
6d10ca09b4 [ base ] add Show for Ordering 2022-01-19 22:12:36 +00:00
octeep
f7bcd1f0b2 make readBufferData return the number of bytes that have been read 2022-01-19 17:35:14 +00:00
Robert Wright
76d1936fad Add Singleton type 2022-01-19 14:22:40 +00:00
Mathew Polzin
4220c644cf
Add a few missing NodeJS FFI functions to System (#2271)
* support for system command via node backend.

* Add env var set/unset

* fix env unset function

* Update libs/base/System.idr

* modify system test to cover node and chez.

* Add base tests for env get/set
2022-01-18 22:43:03 -08:00
Guillaume Allais
ffff9bc2e1 [ new ] die 2022-01-18 18:44:36 +00:00
Ellis Kesterton
f93e1c4eac
Change associativity for System.Path operators (#2240)
Co-authored-by: eayus <erk@st-andrews.ac.uk>
2022-01-06 18:23:51 +00:00
Mathew Polzin
1b4811b1ed
[cleanup] Unhide string module (#2230)
* unhide string lines/unlines functions and clean up a bit.
* skip the extra newline now that unlines adds one at the end.
2022-01-06 10:34:15 +00:00
Nick Drozd
ec5f40eec7
Injective follow-up (#2155) 2022-01-05 09:40:23 +00:00
Ellis Kesterton
f016a81e37
Add 'tryParse' function to 'System.Path' (#2234) 2021-12-30 16:23:45 -08:00
Mathew Polzin
266e06cab7
[cleanup] Small round of unused import culling. (#2231)
* small round of unused import culling.

* and also the libraries.
2021-12-29 20:42:29 -08:00
Denis Buzdalov
7834539240
[ re #238 ] Fix program error condition of git diff call in Golden (#2119)
* [ fix ] Fix returned status of the `system` function

* [ re #238 ] Fix program error condition of `git diff` call in `Golden`

According to documentation, not only negative exit code means error
2021-12-22 13:33:37 -08:00
alissa-tung
158cb1c75e [ nodejs ] pid 2021-12-22 22:25:21 +08:00
Denis Buzdalov
a09c5082c5
[ base ] Use Fin n as index in Bits (#2192) 2021-12-16 18:26:52 +00:00
teggot
d3aed0404c
[ fix #1959 ] use modern record update syntax (#2196) 2021-12-16 18:23:18 +00:00
Balazs Komuves
3463adbc48
[ fix #2032 ] Slow typechecking on Int operation when Data.Fin.fromInteger is in scope (#2189) 2021-12-13 13:47:53 +00:00
Balazs Komuves
c3ec522077
[ fix #1404 ] Totality annotation for data type definitions (#2179)
Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>
Co-authored-by: stefan-hoeck <hock@zhaw.ch>
2021-12-08 16:08:26 +00:00
Kamil Shakirov
ce67a2edd5 [ fix ] Re-add Pretty instances for IntX 2021-12-08 14:58:32 +00:00
André Videla
10b9685e4b
Injective interface and its implementations (#2114)
Co-authored-by: Nick Drozd <nicholasdrozd@gmail.com>
2021-11-26 10:55:17 +00:00
Denis Buzdalov
f1941cecac [ cleanup ] Remove piece of dead code from prelude 2021-11-26 10:14:47 +00:00
G. Allais
059f74ad0b
[ fix #1861 ] rewrite_impl is linear (#2150) 2021-11-25 17:07:05 +00:00
Nick Drozd
9e0676597d Cut relation implicit args 2021-11-25 00:26:57 +00:00
Guillaume ALLAIS
a91fdae426 [ base ] generalise Data.List type signatures 2021-11-24 19:58:35 +00:00
stefan-hoeck
c504a26bc8 [ type inference ] use determining parameter in relation interfaces 2021-11-22 09:52:32 +00:00
Mathew Polzin
1576a578a0
[ cleanup ] Remove unused imports (#2123)
* contrib library unused import removal
* remove a few unused imports.
* another round of unused import removal
* another round of unused import deletion.
* another round of unused import deletion.
2021-11-18 16:47:36 +00:00
Thomas Dziedzic
c31cd9513f make Data.List1.length public 2021-11-18 16:42:49 +00:00
Thomas Dziedzic
88f8f3df8e implement Data.List1.length 2021-11-18 08:38:00 +00:00
Mathew Polzin
0eba4c691e
Add %deprecate pragma (#2086) 2021-11-17 10:41:03 +00:00
André Videla
cc45ff957a
Merge pull request #2085 from andrevidela/string-parser-position
Show the line and column in diagnostic message in String.Parser
2021-11-15 11:09:57 +00:00
Denis Buzdalov
ba180706d6 [ ux ] Make expected and given results be printed colourful in Golden 2021-11-11 23:25:11 +00:00
Kamil Shakirov
ae411fe756 [ doc ] Mark code blocks as Idris code 2021-11-11 18:55:11 +00:00
Mathew Polzin
d2ce85ea05
Merge pull request #2096 from madman-bob/system-run
Add the `System` `run` function
2021-11-10 08:58:39 -08:00
Robert Wright
2ee10d9b34 Add Alternating List odds and evens functions 2021-11-10 08:40:25 +00:00
André Videla
9e6678e3d3
Merge pull request #2102 from madman-bob/list-singleton
Add List singleton function
2021-11-10 00:46:40 +00:00
André Videla
7f932036e9 Show the line and column in diagnostic message
This also updates the error message of some common combinators
2021-11-10 00:44:09 +00:00