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
André Videla
72270962fc
Merge pull request #3043 from dunhamsteve/issue-3030
...
[ fix ] Totality checker misses indirect references to negative data
2023-09-08 12:55:20 +01:00
Steve Dunham
8c14e9527b
[ test ] move test to correct location
2023-09-07 20:26:18 -07:00
Steve Dunham
e4fe90e1a3
Merge branch 'main' into foo
2023-09-07 20:19:26 -07:00
Guillaume Allais
b4d7bba550
[ cleanup ] use default arguments
...
This simplifies most calls to `testsInDir`.
2023-09-07 14:57:22 +01:00
Robert Wright
cf73efe8e0
Update linter config
2023-09-07 14:57:22 +01:00
Robert Wright
424bc20c27
Group tests by directory
2023-09-07 14:57:22 +01:00
Robert Wright
2bde9104e0
Add filter_test_dir test utility
2023-09-07 14:57:22 +01:00
Robert Wright
61878ef1b6
Remove trivial testing input files
2023-09-07 14:57:22 +01:00
Robert Wright
09466a96bb
Add testing utilities script
2023-09-07 14:57:22 +01:00
G. Allais
c52b029986
[ new ] function options for case blocks ( #3062 )
2023-09-01 11:35:52 +01:00
Aleksei Volkov
af7ba2fa67
[ ttc ] Compare modification time with nanosecond precision ( #3046 )
2023-08-31 11:55:57 +01:00
