idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-21 02:31:50 +03:00
Code Issues Projects Releases Wiki Activity
3,575 Commits 6 Branches 9 Tags 115 MiB
eb9d4d65a5
Commit Graph

3575 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
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
Walter Smuts
98e5615dbc Typos: change all uses of inferable to inferrable 
Achieves consistency...
 2023-06-08 13:45:57 +02:00
Walter Smuts
e86420f710 Typos: specificy -> specify 
Audit of "docs/" typos that did not have single match.
 2023-06-08 13:41:58 +02:00
Walter Smuts
ab2d828887 Typos: Run 'typos -w' command over docs/ 
Only running over "docs/" directory since it will likely have the
largest postivie impact and cause fewest issues.

Typos will do simple find-and-replace when it detects a word not in it's
dictionary. It does not have any regard for formatting based on
surrounding context. Care must be taken not no merge variable names in
same scope etc.

Typos can be driven by Github Actions:
https://github.com/crate-ci/typos/blob/master/docs/github-action.md

Tool: https://github.com/crate-ci/typos
 2023-06-08 13:41:54 +02:00
Leo
31c17ebec2
Add Pack to list of package managers (#2986) 
* Add Pack to list of package managers

* Mention only Pack as package manager

Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>

---------

Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>
 2023-06-02 07:27:12 +01:00
Aleksei Volkov
e594669210
[ fix #1878 ] Programmer-provided terms should be alwaysReduce (#2977) 
* [ fix ] Programmer-provided terms should be alwaysReduce

This ports Edwin's commit that fixes the original issue back to Idris

Co-authored-by: Edwin Brady <ecb10@st-andrews.ac.uk>

* [ tests ] Added regression test for #1878

* Updated CHANGELOG.md and CONTRIBUTORS

---------

Co-authored-by: Edwin Brady <ecb10@st-andrews.ac.uk>
 2023-06-01 17:08:02 +01:00
Justus Matthiesen
00af44c708
Ignore UseSide annotation in non-linear as-patterns (#2984) 
Co-authored-by: Aleksei Volkov <volkov.aa@phystech.edu>
 2023-06-01 14:34:57 +01:00