Justus Matthiesen
8a9bf396ea
[ new ] semiring instance for SizeChange
2023-11-06 20:10:21 +00:00
Justus Matthiesen
aac6e8600c
[ new ] sparse matrices
2023-11-06 20:10:21 +00:00
Justus Matthiesen
4f7f5a2ed4
[ cleanup ] use information order for SizeChange
2023-11-06 20:10:21 +00:00
Justus Matthiesen
d76361e0f6
[ refactor ] move SizeChange to a separate file
2023-11-06 20:10:21 +00:00
Thomas E. Hansen
db87cef0ad
[ doc ] Headings for envvars based on use-time
...
Some envvars are only used at build-time, some only at runtime, and lots
are used at both. This clearly cagetorises them accordingly in the docs.
2023-11-01 09:41:22 +00:00
Mathew Polzin
7b0a1b4013
Update ffi.rst
2023-10-30 17:29:20 -05:00
Denis Buzdalov
64ad807f83
[ deriving ] Try to reduce a type before searching it's showable
2023-10-30 10:07:39 +00:00
G. Allais
bee59d5fde
[ fix ] missing modules in .ipkg files ( #3124 )
...
Additionally, we now have bash options to make sure we will fail hard were
this situation to arise once again.
2023-10-27 20:37:00 +01:00
G. Allais
e2d2710504
[ linear ] introduce mapFst, mapSnd ( #3121 )
...
* [ linear ] introduce mapFst, mapSnd
* [ new ] add insertAt, the inverse to lookup
2023-10-27 13:22:13 +01:00
Steve Dunham
73507a826b
[ cleanup ] remove duplicate copy of header parsing ( #3122 )
2023-10-27 13:08:17 +01:00
Steve Dunham
58ec72e0f4
[ ci ] Run a brew update during ci
2023-10-27 07:55:44 +01:00
Denis Buzdalov
5f29b0b9c5
[ elab ] Add an ability to inspect in which function we currently are
2023-10-26 15:42:26 +01:00
Denis Buzdalov
50a579fa18
[ elab ] Implement an operation of returning referred defs of a def
2023-10-26 15:42:26 +01:00
G. Allais
9f93d4c1ec
[ doc ] Improve the landing page ( #3119 )
...
* [ doc ] Improve the landing page
1. Mentioning the network package too
2. Adding the Idris logo to the page
2023-10-26 10:35:01 +01:00
Adowrath
ea093ffaed
[ warning ] for incompatible visibilities on forward decls and definitions. ( #3063 )
2023-10-25 11:24:43 +01:00
Denis Buzdalov
305604d243
[ base ] Implement a bunch of standard interfaces for Data.These ( #3117 )
...
* [ base ] Implement a bunch of standard interfaces for `Data.These`
* [ base ] Add couple of eliminators with default values for `These`
2023-10-25 11:15:28 +01:00
CodingCellist
46be3b8082
[ ci ] Update deploy-action in ci-idris2-and-libs.yml ( #3115 )
2023-10-23 15:26:20 +01:00
Raffi Sanna
4097e6c993
Switch from 'fast' string functions to normal string functions
2023-10-23 12:01:13 +01:00
CodingCellist
fcecb165b9
[ doc ] Document failing blocks ( #3114 )
2023-10-23 11:40:18 +01:00
Raffi Sanna
f694e5e2f0
Use do notation in some
2023-10-19 08:45:33 +01:00
Denis Buzdalov
6c35157087
[ ux ] Make isType fail with positioned errors
2023-10-17 18:05:54 +01:00
Denis Buzdalov
f64047b9ac
[ safe ] Set deriving escape hatches to be marked as %unsafe
2023-10-17 18:05:54 +01:00
Denis Buzdalov
2358a74a29
[ base ] Implement Zippable for several standard types + small cleanup
2023-10-16 22:41:55 +01:00
0xd34df00d
7c8076c149
[ base ] Relevant and irrelevant traversals for Data.Vect.Quantifiers.All
2023-10-16 09:49:22 +01:00
Aleksei Volkov
3e5d8a54d4
[ fix ] Prevent relative path traversal in elaborator scripts
2023-10-16 09:43:22 +01:00
Steve Dunham
c04404a95b
[ fix #3097 ] Fix issues parsing %logging followed by named impls ( #3098 )
...
Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>
2023-10-13 19:02:58 +01:00
Denis Buzdalov
419a440dad
[ impl ] Support default implicits in named implementations ( #3100 )
2023-10-13 15:26:42 +01:00
0xd34df00d
f2a95071a1
[ base ] Add Data.Vect.Quantifiers.All.remember, the inverse to forget ( #3096 )
...
Co-authored-by: Guillaume Allais <guillaume.allais@ens-lyon.org>
2023-10-13 15:26:24 +01:00
Stefan Höck
7fbbb030df
[ new ] add Data.List.grouped function ( #3089 )
2023-10-13 13:48:15 +01:00
Denis Buzdalov
f7d4b7f4ed
[ base ] Add a bridge between MonadState and Ref
2023-10-13 13:47:31 +01:00
Denis Buzdalov
6815aefbe0
[ elab ] Implement file operations, e.g. applicable for type providers
2023-10-13 13:26:46 +01:00
Denis Buzdalov
cbbd0c8caa
[ elab ] Make %macro-function be callable without the extension
2023-10-11 13:20:12 +01:00
0xd34df00d
32b639ca3c
[ base ] Prove anyToFin preserves the property witnessed by Any
2023-10-09 15:03:55 +01:00
0xd34df00d
8d5caaa137
[ base ] Add anyToFin converting a Vect's Any to its index
2023-10-09 15:03:55 +01:00
Denis Buzdalov
1256ded110
[ elab ] Implement Ord for Count
2023-10-04 16:31:38 +01:00
Denis Buzdalov
a5b02747b6
[ re #3066 ] Make the rest of tests to use the same form as the others
2023-10-04 14:34:03 +01:00
Denis Buzdalov
567f019230
[ test ] Set IDRIS2_PREFIX to a local dir when testing
2023-10-04 14:34:03 +01:00
Denis Buzdalov
847b525189
[ re #3067 , readme ] Fix the build badge in the readme
2023-10-04 12:06:42 +01:00
Denis Buzdalov
46a2dc1c1f
[ doc, tiny ] Correct wrong directive for unbound implicits turning off
2023-10-01 07:16:20 +01:00
Denis Buzdalov
f3eff838b2
[ perf ] Do not split tree too early
2023-10-01 07:16:20 +01:00
Denis Buzdalov
276d41d86c
[ new ] Implement Sized for Seqs
2023-10-01 07:16:20 +01:00
Denis Buzdalov
0c40a76c2c
[ re #2884 ] Move existing test to an appropriate category
2023-10-01 07:16:20 +01:00
Steve Dunham
46483fd120
[ fix ] support .lidr.md and .lidr.tex extensions ( #3071 )
2023-09-25 22:25:26 +01:00
Denis Buzdalov
3886200d29
[ fix ] Make traverse and friends lazy for LazyList
2023-09-25 19:51:17 +01:00
Denis Buzdalov
6dc06cd67d
[ base ] Add update functions to sorted maps
2023-09-23 22:47:05 +01:00
Denis Buzdalov
a643e3af62
[ elab ] Print script's FC in the bad elaboration script error
2023-09-22 11:55:34 +01:00
Joel Berkeley
f6c000e27e
Fix typo in namespace for [bi]traversable composition
2023-09-20 09:15:56 +02:00
Thomas E. Hansen
dc79c6dd05
[ ci ] re 3067: fix CI on main branch
...
The extra CI jobs introduced in #3067 work fine as long as 'main' is not
the checked out branch. This is due to the fetch to a new branch, which
git does (reasonably) not allow when you're trying to fetch 'main' into
a new branch that's also called 'main'. In this case, we should just
`git pull origin main`, which is what the script now (hopefully) does.
2023-09-15 12:05:10 +02:00
Steve Dunham
0029257eec
[ fix ] consider nest when guessing scrutinee ( #3070 )
2023-09-14 14:29:41 +01:00
CodingCellist
9d083154a5
Test pack and lsp during CI ( #3067 )
2023-09-13 17:37:49 +01:00
