Denis Buzdalov
cf9a73f86c
[ prelude ] Add some lacking %tcinlines
2023-08-23 11:04:53 +01:00
russoul
ebbae42c85
Add uncons' to base; rewrite head' and tail' in terms of uncons'
2023-08-23 11:04:23 +01:00
Janus Troelsen
694b1650c8
[ racket ] Add library loading ( #3049 )
2023-08-23 11:04:01 +01:00
Aleksei Volkov
115c9e0889
[ unelab ] Properly unelaborate metavariables originating from %search ( #3055 )
...
* [ unelab ] Properly unelaborate `%search`
* [ test ] Added regression test that checks quotation of `%search`
2023-08-23 08:02:11 +01:00
Jens Petersen
48dbc3251b
implement DESTDIR support for distros
...
both 'make install' and 'idris2 --install*' should respect DESTDIR now
2023-08-22 16:44:13 +01:00
André Videla
86c53e6071
Merge pull request #3045 from mars0i/main
...
Add documentation for Not.
2023-08-16 21:43:47 +09:00
Marshall Abrams
bdb6531b86
Add documentation for Not.
2023-08-15 20:07:21 -05:00
Steve Dunham
badf1e98c8
[ base ] Make foldr1 and foldr1By public
2023-08-07 08:10:35 +01:00
Steve Dunham
3ce8b9f9cb
[ fix ] Pin chez v9.5.8a in windows CI
2023-08-06 09:51:40 +01:00
Steve Dunham
bde1a66075
[ fix ] Fix pattern match issue with function application in Refl ( #3027 )
2023-08-04 13:46:04 +01:00
Steve Dunham
f0f776c288
[ error ] Improve error messages for Delay &co
2023-08-04 13:39:39 +01:00
Robert Wright
3c61471da3
Erase additional PreorderReasoning arguments
2023-08-04 13:37:46 +01:00
Steve Dunham
dc43ce2056
[ fix ] fix scheme002 test on windows
2023-08-03 23:16:14 +01:00
Denis Buzdalov
b7bda5e96d
[ docs ] Fix the formatting warning in the docs
2023-08-01 12:48:33 +01:00
Steve Dunham
b481994bef
[ fix ] Fixes build broken by #3021
2023-08-01 08:01:12 +01:00
scarf
c7abb148e8
feat: even and odd for Nat and Integral ( #3021 )
2023-07-31 08:36:40 +01:00
André Videla
1fa638494d
[ new ] Fixity access modifier ( #3011 )
2023-07-31 08:35:16 +01:00
CodingCellist
51403ab18c
[ fix ] Only set IDRIS2_PREFIX if it is unset (fixes Issue 3022) ( #3024 )
2023-07-31 08:18:15 +01:00
Robert Wright
cbbe761c51
Add fromTTImp, fromName, and fromDecls for custom TTImp, Name, and Decls literals
2023-07-31 08:17:55 +01:00
Saransh Chopra
4fcb0fb4a7
Remove decideLTE ( #3031 )
2023-07-27 08:04:24 +01:00
Wilko Manger
870bc82437
Remove shadowed names in documentation
2023-07-21 15:38:34 +01:00
André Videla
23694c7e5a
Merge pull request #3019 from andrevidela/contributing-updates
...
[ docs ] Update contributing guidelines
2023-07-19 01:35:32 +09:00
André Videla
0ced694d0b
[ docs ] Update contributing guidelines
...
* Don't link to discord. Write a summary instead.
* Move around the intro and the main disclaimer.
2023-07-18 17:27:20 +01:00
André Videla
f125278696
Merge pull request #3007 from stefan-hoeck/constant_fin
...
[ performance ] make Eq and Ord for Fin run in constant time
2023-07-19 01:13:41 +09:00
André Videla
a39bfc6ce3
Merge branch 'main' into constant_fin
2023-07-18 23:46:07 +09:00
Steve Dunham
8d7791ba55
[ base ] Add getTermCols and getTermLines to base library and fix pri… ( #3009 )
2023-07-18 09:42:47 -05:00
André Videla
6be16a3b06
Merge pull request #3017 from dunhamsteve/issue-3016
...
[ fix ] Ensure local defs with no claim are local
2023-07-18 23:40:39 +09:00
Steve Dunham
113c3930f3
[ fix ] deduplicate definedInBlock results
2023-07-16 09:01:13 -07:00
scarf
388d217757
docs: typo in list difference documentation ( #3018 )
2023-07-16 10:39:36 -05:00
Steve Dunham
5165c79b67
[ fix ] Ensure local defs with no claim are local
2023-07-15 18:18:48 -07:00
CodingCellist
6729fa8c89
Revert "Treat unit types as erased in constructors ( #3002 )"
...
This reverts commit 677acf0d84
2023-07-07 17:48:07 +02:00
Zoe Stafford
677acf0d84
Treat unit types as erased in constructors ( #3002 )
...
* Treat unit types as erased in constructors
* Cleanup + dump ttc version
* Update CHANGELOG.md
2023-07-05 19:51:34 +01:00
Katarzyna Marek
5fd5b1e732
improvement: use std lib WellFounded for Sufficient
2023-07-05 16:44:07 +01:00
CodingCellist
18e887389f
[ papers ] Port the first part of "Deferring the details [...]" by Liam O'Connor ( #2974 )
...
Co-authored-by: Guillaume Allais <guillaume.allais@ens-lyon.org>
2023-07-05 16:42:58 +01:00
Noam Yorav-Raphael
d4a8c95fe3
Update docs copyright notice from 2020 to 2023 ( #3001 )
...
Co-authored-by: CodingCellist <teh6@st-andrews.ac.uk>
2023-07-05 16:39:12 +01:00
Robert Wright
754f6af55c
Add orBothFalse proof
2023-07-05 16:36:55 +01:00
Robert Wright
af3c5fd454
Generalize Prelude proof helpers
2023-07-05 16:36:09 +01:00
stefan-hoeck
c1a5be9b5b
[ performance ] make Eq and Ord for Fin run in constant time
2023-07-05 15:58:41 +02:00
Steve Dunham
ecf4765c4b
[ fix ] Fix issue with eager evaluation of crashing functions ( fixes #3003 ) ( #3004 )
...
* [ fix ] Fix issue with eager evaluation of crashing functions
* Mark functions that call unsafe builtins as non-constant
* Better detection of crash primop when deciding if functions can be constant
2023-06-28 08:32:48 +01:00
Denis Buzdalov
5dcf62499d
[ elab ] Make elab scripts be able to record warnings ( #2999 )
2023-06-19 16:34:19 +01:00
André Videla
9f20ba2609
Merge pull request #2918 from buzden/min-max-gen-for-connex
...
[ new ] Add generalisations of `min` and `max` for `StronglyConnex`
2023-06-16 15:27:06 +01:00
André Videla
c6e476ed1a
Merge pull request #2997 from andrevidela/infix-namespace-hiding
...
Infix namespace hiding
2023-06-14 12:29:25 +01:00
Andre Videla
9797a79b53
[ new ] Allow fixities to be hidden with %hide
...
* Change the printing of namespaced operator to show
parenthesis around operators
* Update warning when conflicting fixities are found
* Do not warn about redundant but compatible fixities
2023-06-14 11:19:59 +01:00
André Videla
1fa59f842a
Merge pull request #2926 from Alex1005a/let-in-do
...
Add explicit error when using let-in in do block
2023-06-13 16:21:13 +01:00
Alexander
63fa070efa
add test for parse error let-in in do block
2023-06-13 11:01:42 +03:00
Alexander
a01b7e25d9
[parser] error message if use let-in in do block
2023-06-13 10:35:39 +03:00
André Videla
26c5c4db03
Merge pull request #2970 from WalterSmuts/main
...
Typos: Run 'typos -w' command over docs/
2023-06-12 11:21:23 +01:00
Justus Matthiesen
2733ec2333
[ doc ] add lazy functions to changelog
2023-06-12 11:04:59 +01:00
Justus Matthiesen
6c6867490c
[ test ] lazy functions
2023-06-12 11:04:59 +01:00
Justus Matthiesen
bb6db779ef
[ fix #1066 ] do not insert TForce on LHS
...
When we encounter a delayed (explicit) function type during elaboration
of a LHS, we strip off the delay modality, continue elaboration and return a delayed version of the resulting type.
Note: defining delayed function via pattern matching is not currently
supported. Doing so will require adding a delay marker to LHSs/contexts
familiar from modal type theories. Implicit function are also currently
not supported.
2023-06-12 11:04:59 +01:00
