MithicSpirit
f83ad9ce98
[ base ] Data.SortedSet.leftMost and .rightMost ( #3260 )
...
* [ base ] Data.SortedSet.leftMost and .rightMost
Implement `leftMost` and `rightMost` for `SortedSet` in terms of the
functions with the same name in `Data.SortedMap`.
* contributors
---------
Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>
2024-06-05 12:00:57 +01:00
Joel Berkeley
40d4cd898b
clarify toMaybeT docstring
2024-06-05 11:59:52 +01:00
G. Allais
004f1fd26b
[ new ] Data.SnocList.HasLength from compiler libs ( #3299 )
2024-06-05 11:51:23 +01:00
Denis Buzdalov
a6c5cf5af0
[ fixup #2939 ] Make futures not interfere with optimisations
2024-06-03 15:43:23 +01:00
Stefan Höck
e73ca067ed
[ performance ] a faster implementation of unpack ( #3281 )
...
* [ performance ] a much faster implementation of unpack
* [ fix ] partiality error in Hangman test
* [ test ] add some documentation to the unpack test case
* [ test ] fix expected output of unpack test
2024-05-24 08:06:56 +01:00
Denis Buzdalov
cf68e995c4
[ funext ] Add a proof for funext variants with the other quantities
2024-05-19 15:00:28 +01:00
Steve Dunham
7854bf4ab0
[ fix ] Fix ENOMEM on macos rest runner
2024-04-28 11:10:19 -07:00
stefan-hoeck
e1c5c2fd8e
[ fix ] issue 3266
2024-04-22 15:44:35 +02:00
Ellis Kesterton
2823281af6
Add partiality/delay monad ( #3240 )
2024-04-04 11:53:11 +01:00
André Videla
75032a7164
Emit warning for fixities with no export modifiers ( #3234 )
...
* Emit warning for fixities with no export modifiers
This is to help update all the existing code to program with explicit
fixity export directives in preparation for the behavioral change where
they will become private by default.
2024-04-03 15:41:57 +01:00
G. Allais
2c2aa85048
[ prelude ] the is linear in its input ( #3239 )
...
* [ prelude ] `the` is linear in its input
* [ fix ] eta-expand tests
2024-03-27 14:09:14 +00:00
Mathew Polzin
7ce4c45e82
Complete the relocation of contrib HVect into base as All ( #3191 )
...
* complete the relocation of contrib HVect into base as All
* Frex needs these public exported and that feels reasonable enough to me
* Add CHANGELOG_NEXT entries
2024-03-19 08:22:32 -05:00
Jacob Walters
18b165bede
[ elab ] Let elab scripts access visibility modifiers
2024-03-15 22:41:29 +00:00
Mathew Polzin
7219486aec
Fix ambiguity error with Uninhabited interface implementations. ( #3228 )
2024-03-15 17:21:05 -05:00
Jason Hemann
e6bd13634e
Typo fix in docs for /contrib/Data/Telescope.idr
2024-03-09 17:15:43 +01:00
Jason Hemann
e4337c118b
Typo fix in Data/Vect/Properties/Fin.idr
2024-03-09 13:38:53 +01:00
rvs314
1143718098
Generalize succNotLTEpred ( #3225 )
...
* Don't require a runtime value of `x` for `succNotLTEpred`
* Add `succNotLTEpred` as an instance of `Uninhabited`
* Add contribution to changelog
* Update golden value for test `basic044`
2024-03-07 08:38:28 -06:00
Denis Buzdalov
8144980ae5
[ elab ] Support easy collection of information during TTImp traverse
2024-02-23 11:32:22 +01:00
Ruslan
2e1c3fbf2e
Fix a bug in C implementation of idrnet_recv_bytes (missing flags parameter) ( #3212 )
...
* Fix a bug in C implementation of idrnet_recv_bytes (missing flags parameter)
2024-02-12 11:35:52 -06:00
Denis Buzdalov
9ab96dacd4
[ elab ] Treat map and <*> with no bind in elab scripts runner
2024-01-17 17:45:19 +03:00
Mathew Polzin
073fbef3d1
Remove use of deprecated getByte function ( #3190 )
...
* Add CHANGELOG_NEXT entry
2024-01-14 11:26:51 -06:00
Joel Berkeley
ee18555869
Add (++) for List variation of All ( #3179 )
...
* Add `(++)` for `All` for `List`
* changelog
* contributors
* review changes
* update comment
* update comment
* match TODO style
* disambiguate the right one
* further comment changes
2024-01-01 21:03:13 -06:00
Denis Buzdalov
d5d4b2a9ae
[ contrib ] Support options parsing errors in a backward-compatible way
2023-12-30 14:22:51 -06:00
Denis Buzdalov
1b627b0b78
[ contrib ] Support alternative getOpt working nicely with parse errors
2023-12-30 14:22:51 -06:00
Denis Buzdalov
3fe95d469a
[ interpolate ] Implement Interpolation for primitive numeric types
2023-12-29 11:17:31 -06:00
Denis Buzdalov
db4f65bd8d
[ refactor ] Move lazy lists from contrib to base
2023-12-29 09:22:03 -06:00
Denis Buzdalov
0e831ed5ef
[ prelude ] Make able to implement provably total showPrec recursively
2023-12-26 10:16:57 +00:00
Denis Buzdalov
82bb12cf72
[ cleanup ] Post v0.7.0 cleanup
2023-12-25 13:49:26 +00:00
Thomas E. Hansen
ea180d0721
[ rc ] Prepare for 0.7.0
...
A lot more sensible all around : )
2023-12-22 14:44:30 +01:00
Thomas E. Hansen
a3b078cb0d
[ rc ] For v0.6.9 - to see if the process was right
...
Good luck everybody...
v0.6.9 - Nice! ^^
2023-12-22 14:44:30 +01:00
Denis Buzdalov
da916b68d4
[ fix ] Correctly manage the empty file case while reading a file
2023-12-21 13:30:30 -06:00
Denis Buzdalov
b495fe83f0
[ fix ] Support waiting for popen2-created processes
...
This fixes problem of creation the garbage of zombie processes on POSIX
systems. This also makes behaviour of `popen2` identical in Windows,
namely, all resources are freed only when waiting, giving at the same
time an ability to observe the exit code afterwards.
2023-12-19 23:03:31 +03:00
Denis Buzdalov
eddcbcdc75
[ base ] Add modifyRef into the Ref interface
2023-12-08 18:54:57 +00:00
Denis Buzdalov
8557b5b810
[ typo ] Fix a silly typo
2023-12-08 18:54:57 +00:00
Denis Buzdalov
e3ff0b7786
[ minor ] Remove a compilation warning from prelude
2023-12-08 18:54:57 +00:00
russoul
f2e6dc4313
Add dependent congruence of arity 1 and 2 for heterogeneous equality
2023-11-30 10:08:54 +00:00
Andor Penzes
82e4fd9da7
Add foldrImplGoLemma to Data.Vect ( #2835 )
...
Co-authored-by: CodingCellist <teh6@st-andrews.ac.uk>
2023-11-30 10:07:41 +00:00
0xd34df00d
6dd25cd9ec
[ base ] Add mapPropertyRelevant, tabulate and (++) for Vect's All
2023-11-30 09:53:05 +00:00
G. Allais
b08efbea40
[ refactor ] split Core.TT ( #3151 )
2023-11-29 20:24:01 +00:00
Denis Buzdalov
2c328a51c0
[ elab ] Support more applicative traversals of TTImp
2023-11-09 22:05:36 +00:00
CodingCellist
d80bc1537d
[ base ] Add bindings for ieee Double number consts ( #3116 )
2023-11-09 14:01:40 +00: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
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
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
Raffi Sanna
4097e6c993
Switch from 'fast' string functions to normal string functions
2023-10-23 12:01:13 +01:00
Raffi Sanna
f694e5e2f0
Use do notation in some
2023-10-19 08:45:33 +01:00
