idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-22 11:13:36 +03:00
Code Issues Projects Releases Wiki Activity
3,102 Commits 6 Branches 9 Tags 115 MiB
0e657aeba1
Commit Graph

3102 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
teggot
d3aed0404c
[ fix #1959 ] use modern record update syntax (#2196) 2021-12-16 18:23:18 +00:00
Ruslan
516cb4a690
Rename lp/loadpackage to package (#2198) 
Also clarifying the doc-string of `:loadpackage`
 2021-12-16 15:58:29 +00:00
Guillaume ALLAIS
6b1c7741e7 [ cleanup ] using whenJust in Driver 
Spotted while reading some unrelated code.
 2021-12-16 15:57:05 +00:00
Guillaume ALLAIS
36918e6186 [ fix ] isImplicit now works for all binders 2021-12-13 20:29:12 +00:00
Balazs Komuves
3463adbc48
[ fix #2032 ] Slow typechecking on Int operation when Data.Fin.fromInteger is in scope (#2189) 2021-12-13 13:47:53 +00:00
octeep
c14ce31db8 Fix compilation on OpenBSD 
Co-authored-by: Johann Rudloff <johann@sinyax.net>

Co-authored-by: Johann Rudloff <johann@sinyax.net>
 2021-12-12 11:42:33 -08:00
Balazs Komuves
6cc20a9974
[ fix #2138] Add an %unhide pragma (#2181) 
* add %unhide pragma

* add a test case

* clean up

* more consistent English usage (+fix some typos)

* add a warning for unhiding not-already-hidden names

* move `unhide` (and `hide`) to the bottom of the source file to avoid having to forward-declare `recordWarning`
 2021-12-11 18:03:36 -08:00
John Mager
9b2811f263 Make RefC search for files in data dirs 
Previously, the RefC files were located in IDRIS2_PREFIX. This is
decoupled to allow users to change the prefix (for ad-hoc library
install locations, for example).
 2021-12-10 14:30:46 +00:00
Balazs Komuves
c3ec522077
[ fix #1404 ] Totality annotation for data type definitions (#2179) 
Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>
Co-authored-by: stefan-hoeck <hock@zhaw.ch>
 2021-12-08 16:08:26 +00:00
Kamil Shakirov
ce67a2edd5 [ fix ] Re-add Pretty instances for IntX 2021-12-08 14:58:32 +00:00
Guillaume ALLAIS
dd3df5da98 [ fix ] highlighting 'as' & 'off' keywords 2021-12-07 18:02:59 +00:00
Balazs Komuves
e511bc6884
[ fix #2098 ] Allow unclosed comment blocks (#2173) 2021-12-07 15:46:38 +00:00
Guillaume ALLAIS
6b92fda5bd [ ci ] Add idris2-elab-util to the libs roster 
[ci: libs]
 2021-12-07 15:15:31 +00:00
Guillaume ALLAIS
816240d93e [ cleanup ] lift quoteX patterns to toplevel 2021-12-07 11:00:50 +00:00
Balazs Komuves
5e775aaa41
[ fix #1945 ] Add default support for record fields (#2175) 2021-12-06 21:21:42 +00:00
Balazs Komuves
3f3912e934
[ fix #2065 ] Use postfix projections if prefix ones are off (#2169) 2021-12-06 18:14:13 +00:00
Edwin Brady
e0c916863c
Fix for incremental builds (#2168) 
When we're inlining, since we only have the current module, we might
encounter names we don't have definitions for. In this case, we need to
leave the arity alone, since the module it originates from will have set
it correctly.

This is tricky to test in isolation, and ideally needs something in CI
for a full incremental build (which would have caught the problem!). I
don't have time right now, but let's at least see if this breaks
anything else for now.
 2021-12-04 20:51:59 +00:00
Guillaume ALLAIS
6f3ef813b1 [ refactor ] use a snoclist internally 2021-12-02 12:49:07 +00:00
Guillaume ALLAIS
32140f577f [ fix ] resugaring of snoc lists 2021-12-02 12:49:07 +00:00
Guillaume ALLAIS
5bf88ceedc [ doc ] more documentation for symbols 2021-12-01 13:35:04 +00:00
André Videla
10b9685e4b
Injective interface and its implementations (#2114) 
Co-authored-by: Nick Drozd <nicholasdrozd@gmail.com>
 2021-11-26 10:55:17 +00:00
Denis Buzdalov
f1941cecac [ cleanup ] Remove piece of dead code from prelude 2021-11-26 10:14:47 +00:00
G. Allais
059f74ad0b
[ fix #1861 ] rewrite_impl is linear (#2150) 2021-11-25 17:07:05 +00:00
Guillaume ALLAIS
500df117c1 [ fix #1741 ] Do not replace names in as-patterns 2021-11-25 16:04:44 +00:00
Guillaume ALLAIS
56e599de9c [ re #1987 ] test case 2021-11-25 15:12:54 +00:00
Nick Drozd
9e0676597d Cut relation implicit args 2021-11-25 00:26:57 +00:00
Guillaume ALLAIS
8e8988ff5a [ re #1191 ] test case 2021-11-24 21:15:43 +00:00
Guillaume ALLAIS
662f1eabc5 [ re #215 ] test case 2021-11-24 20:28:07 +00:00
Guillaume ALLAIS
a91fdae426 [ base ] generalise Data.List type signatures 2021-11-24 19:58:35 +00:00
Guillaume ALLAIS
63bf9f2900 [ re #1852 ] Partial fix without the Hole UN refactoring 2021-11-24 10:54:32 +00:00
Denis Buzdalov
5c5b3a2ae7 [ cosmetic ] Correct one error output 2021-11-23 16:42:51 +00:00
Denis Buzdalov
ab3862798b [ fix ] Use right reflection constructor name for unambiguing with 2021-11-23 16:42:51 +00:00
Denis Buzdalov
ccdd049335 [ cleanup ] Remove small code duplication 2021-11-23 16:42:51 +00:00
Maciej Barć
7fd9844329 Makefile: bootstrap - check for chez threading support 
Signed-off-by: Maciej Barć <xgqt@riseup.net>
 2021-11-22 12:14:04 +00:00
claymager
283f9bd00f
[ fix ] Forbid "." as namespace identifier (#2134) 2021-11-22 12:13:08 +00:00
stefan-hoeck
c504a26bc8 [ type inference ] use determining parameter in relation interfaces 2021-11-22 09:52:32 +00:00
Guillaume ALLAIS
0bc18bd34a [ fix #2072 ] correctly handle fixity in printer 2021-11-19 17:42:07 +00:00
Guillaume ALLAIS
f99b875d7e [ fix #2095 ] error on duplicated updates 2021-11-19 16:30:35 +00:00
gemmaro
c7df41958c [ mkdoc ] Wrap declaration part in <code> tag 2021-11-18 18:19:38 +00:00
G. Allais
489e8c7cbc
[ re #2038 ] doc for reserved symbols (#2126) 2021-11-18 18:13:20 +00:00
Mathew Polzin
1576a578a0
[ cleanup ] Remove unused imports (#2123) 
* contrib library unused import removal
* remove a few unused imports.
* another round of unused import removal
* another round of unused import deletion.
* another round of unused import deletion.
 2021-11-18 16:47:36 +00:00
Thomas Dziedzic
c31cd9513f make Data.List1.length public 2021-11-18 16:42:49 +00:00
Thomas Dziedzic
88f8f3df8e implement Data.List1.length 2021-11-18 08:38:00 +00:00
Guillaume ALLAIS
686a52fb09 [ fix #2122 ] Normalise source directory "." away 2021-11-17 11:55:01 +00:00
Ben Hormann
d1e90a5b8e
[ performance ] bitops arithmetic speedup (#2081) 2021-11-17 11:54:19 +00:00
Denis Buzdalov
a4eb8b2ec3 [ doc ] Fix a complain of not being in a toctree 2021-11-17 10:50:49 +00:00
Mathew Polzin
0eba4c691e
Add %deprecate pragma (#2086) 2021-11-17 10:41:03 +00:00
André Videla
cc45ff957a
Merge pull request #2085 from andrevidela/string-parser-position 
Show the line and column in diagnostic message in String.Parser
 2021-11-15 11:09:57 +00:00
Denis Buzdalov
ba180706d6 [ ux ] Make expected and given results be printed colourful in Golden 2021-11-11 23:25:11 +00:00
Kamil Shakirov
ae411fe756 [ doc ] Mark code blocks as Idris code 2021-11-11 18:55:11 +00:00