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
Stefan Höck
f1d56a4e0f
[ syntax ] Namespaced idiom brackets ( #2284 )
2022-01-24 16:18:36 +00:00
James Cook
e82600c4d6
[ opt ] transform rule making List.length tail-recursive. ( #2100 )
2022-01-24 16:12:29 +00:00
octeep
f137d96cd6
update refc/buffer to check how many bytes have been read
2022-01-24 15:58:32 +00:00
Mathew Polzin
35a84e505d
[ fix #2033 ] determining when to rebuild modules ( #2188 )
2022-01-21 10:26:20 +00:00
stefan-hoeck
b50ecb7bc2
[ fix ] add let in JS array conversion
2022-01-21 09:55:34 +00:00
Guillaume Allais
877025d524
[ fix ] properly decorating pragmas / keywords
2022-01-20 17:55:09 +00:00
stefan-hoeck
1b3be25075
[ breaking, totality ] fGetLine should be covering
2022-01-20 17:48:11 +00:00
Jason Dagit
50c5be30d7
RefC: add test for issue1778
2022-01-20 14:10:57 +00:00
Jason Dagit
89aa6e5e6c
RefC: Better detection for tail calls in cases
2022-01-20 14:10:57 +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
dc25e8f694
Rename RefC extension function stubs
2022-01-20 11:27:30 +00:00
Robert Wright
d85016b64d
Add Fin modular arithmetic Num instance
2022-01-20 10:13:20 +00:00
Mathew Polzin
6f405c9e91
[ new ] Add fixities' FC to the syntax info. ( #2264 )
2022-01-20 10:08:41 +00:00
Mathew Polzin
e7ed760016
[ new ] optional language version field to ipkg files. ( #2256 )
2022-01-20 10:05:53 +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
Trevor Arjeski
0d58282087
Update typedd.rst - Exercise 2 of 8.2.5 ( #2266 )
2022-01-16 23:56:38 -08:00
Edwin Brady
26a47ddafe
Make prim_js2idris_array iterative ( #2267 )
...
I was getting a stack overflow on the tailrec002 test, caused by this
primitive being recursive. I've made it iterative. I'm no JS expert but
I've tested its behaviour against the old version.
2022-01-16 19:15:26 +00:00
Zoe Stafford
3ef46f639e
Merge pull request #2260 from vincentdehaan/fix-docs
...
Minor fix in documentation
2022-01-11 22:27:06 +00:00
Vincent de Haan
3a38424e69
Minor fix in documentation
2022-01-11 22:36:22 +01:00
Jason Dagit
1d7207fe05
[ fix #2202 ] Use SnocList in parser state to avoid quadratic slowdown ( #2203 )
...
Co-authored-by: Guillaume Allais <guillaume.allais@ens-lyon.org>
2022-01-11 16:06:19 +00:00
