idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-09-19 09:17:29 +03:00
Code Issues Projects Releases Wiki Activity
3,531 Commits 5 Branches 9 Tags 121 MiB
cf4c87cc71
Commit Graph

3531 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
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
0b3e04aef0 update tests for DCon in size change 2023-08-12 13:55:07 -07:00
Steve Dunham
878187d7f7 [ fix ] Totality checker misses indirect references to partial data 2023-08-12 12:57:28 -07: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