idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-11 14:23:19 +03:00
Code Issues Projects Releases Wiki Activity
2,916 Commits 5 Branches 9 Tags 109 MiB
4a348c1f95
Commit Graph

2916 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
Mathew Polzin
4a348c1f95 Public export remaining function to allow for proofs involving parsing numbers. 2022-07-18 14:10:05 +01:00
Steve Dunham
c69af04f46
[ fix ] Support multiple ide server instances (#2586) 
* Print the bound ide mode socket instead of the configuration variable.

* Change --ide-mode-socket to choose an open socket instead of using 38398

* [ doc ] Documentation for starting ide-mode
 2022-07-18 14:08:56 +01:00
Steve Dunham
a0d9e2bbba
Update tests using base64 utility to also work on macos (#2536) 
* Update tests using base64 utility to also work on macos

* Fix invocation of base64 in refc/buffer test.
 2022-07-13 06:46:31 -07:00
Nil Geisweiller
da3239bdf5
Update packages.rst (#2588) 2022-07-13 06:25:37 -07:00
ProofOfKeags
68a144bf18
Support System.Signal for node backend (#2556) 
* first pass at signal support for node backend

* change signal values to int's

* implements defaultSignal

* return -1 as expected by calling API if any error is raised by nodejs runtime

* finishes signal support for nodejs

* extract repetitive foreign import identifiers

* fix comments
 2022-07-10 10:18:58 +01:00
Zoe Stafford
8658351b94
Merge pull request #2583 from dunhamsteve/dumpanf 
Fix the --dumpanf command line switch.
 2022-07-10 10:17:46 +01:00
Steve Dunham
32a877c3d4 Fix the --dumpanf command line switch. 2022-07-09 13:18:29 -07:00
G. Allais
1f41c8b44d
[ close #647 ] Already fixed (#2581) 2022-07-08 14:16:25 +01:00
Guillaume Allais
ac2ef882f6 [ fix #2573 ] Solve constraints before looking at eq type 2022-07-07 20:36:05 +01:00
Guillaume Allais
19bc798952 [ re #2526 ] Update golden value 2022-07-07 20:34:54 +01:00
Locria Cyber
05737b25fb Allow to specify --inc when building package 2022-07-07 17:34:41 +01:00
stefan-hoeck
ea6f9975cf [ cleanup ] add proper depends field to network.ipkg 2022-07-07 17:24:54 +01:00
Guillaume Allais
d19dbfffff [ fix #2229 ] better warning 2022-07-07 16:42:34 +01:00
Guillaume Allais
8b20da7e39 [ cleanup ] remove TT from base 
As discussed with edwin, let's get rid of the external TT type.
There is no way to get your hands on a TT value anyway so this
should not change anything.
 2022-07-07 16:42:19 +01:00
Denis Buzdalov
c03a39789f [ breaking ] Make arguments of runRWST like in other transformers 
Put the `RWST` argument to be the last one. This makes such functions
to be easier used in point-free compositions and to be easily
interchangeable with existing `runStateT`-like functions.
 2022-07-07 15:19:41 +01:00
G. Allais
4874bf2114
[ fix ] handle implicit arguments in Deriving.Functor (#2572) 2022-07-07 09:55:13 +01:00
Stefan Höck
5a962929e7
[ fix ] issue 2537 (#2538) 
Co-authored-by: Zoe Stafford <zoepolarsax@gmail.com>
 2022-07-07 09:54:52 +01:00
Guillaume Allais
7db20d38a3 [ cleanup ] Fewer assert_total in deriving Functor 2022-07-04 12:03:49 +01:00
G. Allais
aeeb338e6c
[ new ] deriving Functor (#2568) 2022-07-04 08:58:18 +01:00
Jeroen de Haas
ea7e43ad74 [doc] Remove implicit argument in documentation for parseDouble 2022-07-03 22:00:31 +01:00
Ruslan
dbba32ea09
Fix an eta issue in elaborator-reflection (#2449) 
Co-authored-by: Guillaume Allais <guillaume.allais@ens-lyon.org>
Co-authored-by: Denis Buzdalov <public@buzden.ru>
 2022-06-30 22:01:31 +01:00
Denis Buzdalov
38caff23b8 [ fix ] Make the result Show of case .. of compilable 
1. The arrow was fixed
2. Put explicit type ascription into a comment
3. Don't print type when it was not present in the expression
 2022-06-27 15:32:02 +01:00
Denis Buzdalov
afaa80a5ae [ re #2533 ] Fix printing of lazy values in Show TTImp 2022-06-27 15:32:02 +01:00
G. Allais
4024857d20
[ base ] Various Language.Reflection improvements (#2554) 2022-06-22 13:07:27 +01:00
Denis Buzdalov
e856569d16 [ doc ] Clarify the doc comment of find* functions of SnocList 2022-06-20 12:13:37 +01:00
Denis Buzdalov
113085d0c3 [ base ] Add a function for changing the topmost FC of a TTImp 2022-06-17 19:53:07 +01:00
Denis Buzdalov
bc838467a3 [ base ] Add a function returning Dec for So 2022-06-17 19:52:35 +01:00
Justus Matthiesen
1ae4fdd605 Fix error message for LinearMisuse 2022-06-17 11:48:51 +01:00
Guillaume Allais
e5802204b6 [ fix ] holes in record types 2022-06-17 10:17:40 +01:00
Guillaume Allais
bf3272c344 [ minor ] more magic for name generation 2022-06-17 10:17:40 +01:00
Guillaume Allais
f111838e52 [ cleanup ] move TTC implementations to separate files 2022-06-17 10:17:40 +01:00
Denis Buzdalov
a7fb6722a0
[ re #2533 ] Fix recently added reflection's Show (#2543) 2022-06-16 11:08:51 +01:00
Denis Buzdalov
45579795bc [ elab ] Make any error in elab script to produce a special error type 2022-06-16 09:49:56 +01:00
Denis Buzdalov
742d41f696 [ elab ] Make actual bad script errors be reported so 2022-06-16 09:49:56 +01:00
Denis Buzdalov
df6f4f69cd [ doc ] Add clarification to the doc of a function of Elaboration 2022-06-16 09:49:56 +01:00
Denis Buzdalov
e590014fb7 [ cleanup ] Remove unused expression 2022-06-16 09:49:56 +01:00
G. Allais
bdf3833df5
[ new ] Auto in Agda (+ bonus) (#2541) 
* [ new ] Auto in Agda (+ bonus)

* [ minor ] use DN for more readable terms
 2022-06-16 09:35:45 +01:00
Guillaume Allais
cd324f9ff3 [ base ] Name convenience functions 2022-06-14 16:07:37 +01:00
Guillaume Allais
c9dbc3d743 [ new ] Show implementations for Language.Reflection 2022-06-14 16:07:37 +01:00
Guillaume Allais
381441d849 [ base ] maximum is an upper bound 2022-06-14 16:07:37 +01:00
Guillaume Allais
2060535d08 [ new ] name hints for primitive types 2022-06-14 16:07:37 +01:00
Guillaume Allais
a8fe4a778c [ base ] Show for Constants 2022-06-14 16:07:37 +01:00
Guillaume Allais
128099fd47 [ debug ] better eval logging 2022-06-09 23:09:38 +01:00
Thomas E. Hansen
268a3520f3 [ base ] Port most of List.Quantifiers to List1 
This doesn't include `Interleaving` and `Split`.
 2022-06-09 09:05:10 +02:00
Thomas E. Hansen
5da3bc7d7c [ base ] Port List.Elem to List1 2022-06-09 09:05:10 +02:00
Guillaume Allais
a6a4593aba [ fuzzysearch ] don't print holes 2022-06-08 22:44:55 +01:00
Guillaume Allais
7bd7f1da9c [ fix ] resugaring of DPair 2022-06-08 22:44:55 +01:00
Guillaume Allais
492abf7743 [ new ] better parse error for %language 2022-06-08 22:44:55 +01:00
György Kurucz
79a2f677d4 [ re #1282 ] Improve unelaboration of case expressions 2022-06-08 17:01:36 +01:00
Zoe Stafford
88c18621e6
Merge pull request #2529 from idris-lang/revert-2496-trans-deps 
Revert "Transitive dependencies v2"
 2022-06-08 07:49:58 +01:00