Guillaume Allais
a8fe4a778c
[ base ] Show for Constants
2022-06-14 16:07:37 +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
Denis Buzdalov
a766c628e9
[ base ] Add mapping functions to Data.Vect.Quantifiers
2022-05-27 09:03:28 +01:00
Denis Buzdalov
73608cb264
[ cleanup ] Clean up DecEq implementations with biinjective functions
2022-05-20 11:50:46 +01:00
Denis Buzdalov
d3fa76052b
[ new ] Introduce a Biinjective interface
2022-05-20 11:50:46 +01:00
Denis Buzdalov
a3542ad0cd
[ cleanup ] Make existing equality proofs a bit cleaner
2022-05-20 11:50:46 +01:00
Denis Buzdalov
4032ef2b85
[ base ] Implement equalities for inclusive-or type (These)
2022-05-19 13:37:28 +01:00
Denis Buzdalov
95caed3c4f
[ refactor ] Support alternative equalities for TTImp
2022-05-18 11:12:05 +01:00
Zoe Stafford
71351a6c88
Merge pull request #2476 from Z-snails/bits64-popcount
...
Fix `FiniteBits` for `Bits64`
2022-05-14 14:05:37 +01:00
Zoe Stafford
8a0d75dc6d
Fix FiniteBits for Bits64
2022-05-14 13:12:16 +01:00
Denis Buzdalov
72f0a2ab09
[ re #950 ] Remove redunant legacy data definition
...
`Given` with `Always` from Idris 1 library are completely overridden by
`IsYes` and `ItIsYes` respectively, which have a more common naming.
This, however, may break some very old code (fixed by a trivial rename).
2022-05-14 08:24:20 +01:00
Denis Buzdalov
d037b39e63
[ base ] Add injectivity proof for Yes and No
2022-05-14 08:23:55 +01:00
Joel Berkeley
bf87b623ef
add scanr; scanr1; unsnoc for Vect ( #2471 )
...
* add `scanr` and `scanr1` for `Vect`
* add tests
* tests
* docstring
* typos
* add unsnoc
* simplify unsnoc
* docstring
* typos
2022-05-12 17:54:34 +01:00
Denis Buzdalov
466e14a1e5
[ base ] Add a dependent funext function to the FunExt interface
2022-05-09 18:37:50 +01:00
Edwin Brady
7c5650e94e
Allow functions to be marked for foreign export ( #2433 )
...
* Allow functions to be marked for foreign export
This relies on the backend knowing what to do with such things, but the
general idea is to mark them with '%export "backend:exportedname"' then
'getCompileDataWith', given a back end, will search for every function
that needs to be exported, as well as every function starting from the
expression to be compiled. This will allow Idris functions to be called
from other languages, where a backend supports it.
This is hard to set up a test case for, for the moment, since no
backends actually do anything with it. So consider it a bit of a
placeholder for now.
* Add missing clause to Eq FnOpt
Thanks to @buzden
2022-04-25 13:48:30 +01:00
Denis Buzdalov
77cf47f962
[ re #2423 ] Make Eq implementations in Language.Reflection.TTImp total ( #2430 )
...
* [ re #2423 ] Turn newly added `Eq` implementations to be total
* [ fix ] Add lacking `Eq TTImp` clauses and lacking `Eq` implementations
2022-04-22 18:01:42 +01:00
Zoe Stafford
68bcacf3ec
[base] add missing node ffi functions ( #2427 )
2022-04-22 15:45:52 +01:00
G. Allais
22b98f231e
[ fix ] highlight unambiguous names in `with' ( #2423 )
2022-04-22 13:34:05 +01:00
Denis Buzdalov
71c68d8dcf
[ base ] Add a trace variant easily embeddable to point-free expr
2022-04-14 13:36:14 +01:00
Mathew Polzin
c91a768486
System NodeJS additions ( #2401 )
2022-04-07 10:09:30 +01:00
Thomas E. Hansen
a644a85a57
[ base ] public export quantifier functions
2022-04-04 13:24:12 +02:00
Thomas E. Hansen
dc02e4d822
[ refactor ] Put Vect quantifiers in their own namespaces
...
This makes the code in `Data.Vect.Quantifiers` consistent with the files
`Data.List.Quantifiers` and `Data.SnocList.Quantifiers`.
2022-04-04 13:24:12 +02:00
Denis Buzdalov
1c027d2218
[ re #2370 ] Add forgotten export clause
2022-04-01 12:20:01 +01:00
Denis Buzdalov
f46483106f
[ base ] Add a function extensionality interface
...
Its purpose is to be able to formulate unversally properties which
were true if function extensionality was present in the type system
2022-04-01 11:44:37 +01:00
Daniel Kröni
5eea546642
Aligned the signature of NoMangle from Language.Reflection.FnOpts with that of TTImp.TTImp.FnOpt'.
2022-03-30 13:34:49 +02:00
Jeremy
47cae3459c
[ doc ] for Control.WellFounded ( #2379 )
...
Co-authored-by: Zoe Stafford <36511192+Z-snails@users.noreply.github.com>
2022-03-27 13:05:20 +01:00
Jeremy
394613432f
Add documentation for Control.Monad.* ( #2365 )
...
Co-authored-by: Zoe Stafford <36511192+Z-snails@users.noreply.github.com>
2022-03-25 10:14:25 +00:00
Denis Buzdalov
e8d3d788c1
[ base ] Add some more properties, functions and interface implementations ( #2361 )
2022-03-23 13:33:13 +00:00
Ohad Kammar
d08b827f49
Implement standard List operations for SnocLists ( #2364 )
...
Co-authored-by: Ohad Kammar <ohad.kammar@ed.ac.uk>
2022-03-23 11:14:30 +00:00
Ohad Kammar
319c7f7b86
Move Syntax.PreorderReasoning into base ( #2368 )
2022-03-22 20:58:36 +00:00
Denis Buzdalov
fc38afc144
[ base ] Some properties of List and SnocList ( #2359 )
2022-03-18 08:40:37 +00:00
Joel Berkeley
fc45f7d888
[ base ] add insertAt for List ( #2336 )
2022-03-17 18:23:47 +00:00
G. Allais
a973396567
[ base ] quantifiers for Snoclists ( #2349 )
2022-03-16 15:30:16 +00:00
Denis Buzdalov
05d64483f6
[ refactor ] Factor out a type for primitive types out of Constant
2022-03-10 23:07:20 +00:00
G. Allais
fd02bf8b3e
[ fix #2303 ] remove quadratic unwords ( #2345 )
2022-03-07 18:34:06 +00:00
Robert Wright
6b367010ce
Inline SnocList foldl utility function
...
The scoping of the utility function meant that Idris treats `foldl f z (xs :< x)` and `f (foldl f z xs) x` as two different terms, making proving things about it difficult.
2022-03-07 11:46:43 +00:00
Joel Berkeley
0ab0ecb199
add replaceAt for List ( #2335 )
2022-03-03 23:40:18 +00:00
G. Allais
1011cc6162
[ papers ] Tychonoff (Part I) ( #2332 )
2022-02-24 11:12:53 +00:00
Jan de Muijnck-Hughes
4ba3bb6670
[ fix ] Literate things ( #2312 )
...
Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>
2022-02-18 11:29:52 +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
Guillaume Allais
bec4a0a88e
[ re #499 ] quantity-aware with-clauses
2022-02-09 09:19:40 +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
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
octeep
9a9412e1a2
make writeBufferData return the number of bytes that have been written ( #2276 )
2022-01-25 13:25:06 +00:00
G. Allais
ec5afa5065
[ libs ] move propaganda out of contrib ( #2213 )
2022-01-25 12:25:55 +00:00
