idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-21 10:41:59 +03:00
Code Issues Projects Releases Wiki Activity
9fd28bc130
Idris2/tests/idris2
History
Justus Matthiesen 2b54c23073 [ test ] examples from termination paper
2023-02-08 16:13:04 +00:00
..
api001 [ doc ] add comments to generated javascript (#2594) 2022-07-18 17:30:56 +01:00
basic001 Made unifying error msg nicer. (#1922) 2021-09-15 11:57:50 +01:00
basic002 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
basic003 Fix display of ambiguity errors (#2075) 2021-10-30 23:08:53 +01:00
basic004 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
basic005 Cumulativity preparation: Add field for universe level to TType (#2076) 2021-10-31 00:00:16 +01:00
basic006 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
basic007 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
basic008 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
basic009 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
basic010 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
basic011 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
basic012 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
basic013 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
basic014 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
basic015 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
basic016 [ fix #2072 ] correctly handle fixity in printer 2021-11-19 17:42:07 +00:00
basic017 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
basic018 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
basic019 [ refactor ] Index Pretty over the type of annotations (#2371) 2022-04-27 12:26:59 +01:00
basic020 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
basic021 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
basic022 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
basic023 [ highlighting ] case trees in :di (#2440) 2022-04-29 12:52:23 +01:00
basic024 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
basic025 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
basic026 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
basic027 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
basic028 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
basic029 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
basic030 Made unifying error msg nicer. (#1922) 2021-09-15 11:57:50 +01:00
basic031 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
basic032 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
basic033 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
basic034 Made unifying error msg nicer. (#1922) 2021-09-15 11:57:50 +01:00
basic035 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
basic036 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
basic037 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
basic038 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
basic039 [ doc ] prettier :di (#2356) 2022-03-18 08:45:18 +00:00
basic040 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
basic041 [ fix ] pretty printing of misspellings 2022-04-15 20:18:48 +01:00
basic042 [ fix #2032 ] Slow typechecking on Int operation when Data.Fin.fromInteger is in scope (#2189) 2021-12-13 13:47:53 +00:00
basic043 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
basic044 [ fix ] Remove stray ")" in Show instance for Term (#2611) 2022-08-08 15:24:07 +01:00
basic045 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
basic046 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
basic047 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
basic049 Warning for shadowed local bindings (#2623) 2022-09-07 20:59:28 +01:00
basic050 [ breaking ] remove parsing of dangling binders (#1711) 2021-08-10 19:24:32 +01:00
basic051 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
basic052 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
basic053 move basic053->interpolation002, move basic061->basic053 2021-07-22 12:17:53 +00:00
basic054 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
basic055 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
basic056 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
basic057 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
basic058 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
basic059 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
basic060 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
basic061 [ fix ] Parse let _ = as Let rather than LetPat 2021-08-31 22:50:22 +01:00
basic062 [ fix #1943 ] Allow operator names in named argument applications 2021-09-23 11:41:25 +01:00
basic063 [ re #1944 ] Allow toplevel aliases (#1952) 2021-10-13 21:55:23 +01:00
basic064 [ fix #2072 ] correctly handle fixity in printer 2021-11-19 17:42:07 +00:00
basic065 [ re #215 ] test case 2021-11-24 20:28:07 +00:00
basic066 [ fix #2098 ] Allow unclosed comment blocks (#2173) 2021-12-07 15:46:38 +00:00
basic067 [ fix #2098 ] Allow unclosed comment blocks (#2173) 2021-12-07 15:46:38 +00:00
basic068 [ fix #2138] Add an %unhide pragma (#2181) 2021-12-11 18:03:36 -08:00
basic069 [ new ] __LOC__, __FILE__, __LINE__, __COL__ magic debug strings (#2819) 2022-12-17 18:12:39 +00:00
builtin001 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
builtin002 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
builtin003 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
builtin004 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
builtin005 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
builtin006 Refactor %builtin (#1803) 2021-08-03 14:19:17 +01:00
builtin007 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
builtin008 Refactor %builtin (#1803) 2021-08-03 14:19:17 +01:00
builtin009 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
builtin010 Refactor %builtin (#1803) 2021-08-03 14:19:17 +01:00
builtin011 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
builtin012 Refactor %builtin (#1803) 2021-08-03 14:19:17 +01:00
casetree001 Add Singleton type 2022-01-19 14:22:40 +00:00
casetree002 [ doc ] :printdef for interface implementations (#2340) 2022-03-07 11:47:20 +00:00
casetree003 [ new ] do not split on dotted patterns (#2706) 2022-10-14 16:21:06 +01:00
coverage001 [ re #1632 ] (->) does not unify with any of TCon/Type/PrimVal 2021-09-09 18:37:49 +01:00
coverage002 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
coverage003 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
coverage004 [ new ] semantic highlighting in REPL & holes (#1836) 2021-08-13 16:00:54 +01:00
coverage005 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
coverage006 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
coverage007 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
coverage008 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
coverage009 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
coverage010 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
coverage011 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
coverage012 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
coverage013 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
coverage014 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
coverage015 print location of implicit name shadowing with the warning. (#1968) 2021-10-03 10:15:01 +01:00
coverage016 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
coverage017 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
coverage018 [ highlighting ] case trees in :di (#2440) 2022-04-29 12:52:23 +01:00
coverage019 [ re #1632 ] (->) does not unify with any of TCon/Type/PrimVal 2021-09-09 18:37:49 +01:00
data001 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
data002 [ fix ] respect totality annotations for data (#2862) 2023-01-26 11:03:22 +00:00
debug001 [ re #1282 ] Improve unelaboration of case expressions 2022-06-08 17:01:36 +01:00
docs001 [ doc ] Remove typo from Prelude.plus doc string and 2023-01-24 23:35:03 +00:00
docs002 [ doc ] also display definition's visibility (#2374) 2022-03-24 23:11:10 +00:00
docs003 [ fix ] missing rigs in doc type signatures 2022-05-12 10:25:54 +01:00
docs004 [ IDE ] refine command (#2490) 2022-05-25 11:29:03 +01:00
docs005 [ doc ] return module header docs 2022-03-09 13:31:30 +00:00
dotted001 [ fix 2726 ] more peeling of Erased 2022-10-22 10:07:39 +01:00
error001 Made unifying error msg nicer. (#1922) 2021-09-15 11:57:50 +01:00
error002 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
error003 [ base ] Add some more properties, functions and interface implementations (#2361) 2022-03-23 13:33:13 +00:00
error004 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
error005 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
error006 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
error007 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
error008 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
error009 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
error010 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
error011 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
error012 Rename --consolewidth option to --console-width for consistency 2020-08-19 11:59:31 +01:00
error013 [ doc ] :printdef for interface implementations (#2340) 2022-03-07 11:47:20 +00:00
error014 [ doc ] :printdef for interface implementations (#2340) 2022-03-07 11:47:20 +00:00
error015 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
error016 [ re #1944 ] Allow toplevel aliases (#1952) 2021-10-13 21:55:23 +01:00
error017 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
error018 Move Syntax.PreorderReasoning into base (#2368) 2022-03-22 20:58:36 +00:00
error019 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
error020 Fix error message for incorrect function patterns (#1816) 2021-08-09 10:00:34 +01:00
error021 Abandon ambiguity resolution on undefined name (#1907) 2021-09-07 00:41:08 +01:00
error022 [ fix #1979 ] use virtualised locs rather than EmptyFCs 2021-10-07 16:07:03 +01:00
error023 Implemented %noinline (#2027) 2021-10-19 15:22:36 +01:00
error024 [ parser ] Better error messages for type mismatch on bang expressions 2022-11-01 20:18:33 -07:00
error025 [ error ] Make failing IAlternative w/ FirstSuccess print all errors 2022-11-15 10:28:59 +01:00
error026 [ error ] Fix location of type errors in do block pattern matching 2023-02-04 23:07:49 +00:00
eta001 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
evaluator001 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
evaluator002 [ debug ] Log when stuck because fn out of scope (#2673) 2022-09-22 13:12:47 +01:00
evaluator003 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
evaluator004 [ re #1282 ] Improve unelaboration of case expressions 2022-06-08 17:01:36 +01:00
failing001 [ fix ] make 'failing' whitespace-insentitive 2022-04-07 13:59:27 +01:00
failing002 [ fix ] make 'failing' whitespace-insentitive 2022-04-07 13:59:27 +01:00
failing003 [ fix #2402 ] Check totality before exiting failing block 2022-04-08 13:21:46 +01:00
failing004 [ fix #2821 ] Failing blocks should force delayed holes 2022-12-21 11:16:26 +00:00
golden001 [ cosmetic ] Say when you start compiling the executable (#2714) 2022-10-14 16:21:19 +01:00
idiom001 [ syntax ] Namespaced idiom brackets (#2284) 2022-01-24 16:18:36 +00:00
import001 Disable -Xcheck-hashes, at least for the moment (#1940) 2021-09-20 07:51:33 +01:00
import002 [ re #1944 ] Allow toplevel aliases (#1952) 2021-10-13 21:55:23 +01:00
import003 [ repl ] better printing of holes 2021-09-19 17:49:51 +01:00
import004 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
import005 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
import006 [ fix #1970 ] error on mod self ref (#1977) 2021-10-08 10:09:17 +01:00
import007 [ fix #2053 ] do not show ambiguous private names (#2056) 2021-10-26 15:51:34 +01:00
import008 [ new ] put TTC files in a version-tagged directory (#2684) 2022-11-01 18:11:18 +00:00
inlining001 [ highlighting ] case trees in :di (#2440) 2022-04-29 12:52:23 +01:00
interactive001 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
interactive002 [ re #1852 ] Partial fix without the Hole UN refactoring 2021-11-24 10:54:32 +00:00
interactive003 [ re #1852 ] Partial fix without the Hole UN refactoring 2021-11-24 10:54:32 +00:00
interactive004 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
interactive005 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
interactive006 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
interactive007 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
interactive008 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
interactive009 [ re #1852 ] Partial fix without the Hole UN refactoring 2021-11-24 10:54:32 +00:00
interactive010 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
interactive011 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
interactive012 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
interactive013 [ re #1852 ] Partial fix without the Hole UN refactoring 2021-11-24 10:54:32 +00:00
interactive014 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
interactive015 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
interactive016 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
interactive017 [ re #1282 ] Improve unelaboration of case expressions 2022-06-08 17:01:36 +01:00
interactive018 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
interactive019 [ fix #2721 ] Don't reflow doc lines 2022-10-19 09:09:11 +01:00
interactive020 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
interactive021 [ fix #1744 ] Compare names by root rather than UserName (#1975) 2021-10-05 15:06:16 +01:00
interactive022 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
interactive023 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
interactive024 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
interactive025 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
interactive026 [ fix #1959 ] use modern record update syntax (#2196) 2021-12-16 18:23:18 +00:00
interactive027 [ fix #1744 ] Compare names by root rather than UserName (#1975) 2021-10-05 15:06:16 +01:00
interactive028 [ new ] __LOC__, __FILE__, __LINE__, __COL__ magic debug strings (#2819) 2022-12-17 18:12:39 +00:00
interactive029 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
interactive030 [ fix ] resugaring of DPair 2022-06-08 22:44:55 +01:00
interactive031 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
interactive032 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
interactive033 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
interactive034 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
interactive035 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
interactive036 [ re #1852 ] Partial fix without the Hole UN refactoring 2021-11-24 10:54:32 +00:00
interactive037 [ repl ] better printing of holes 2021-09-19 17:49:51 +01:00
interactive038 Add user hints to expression search 2021-10-24 10:24:22 +01:00
interactive039 [ new ] name hints for primitive types 2022-06-14 16:07:37 +01:00
interactive040 [ fix #2046 ] only refold positive integers as nats (#2064) 2021-10-26 17:16:31 +01:00
interactive041 [ fix #1741 ] Do not replace names in as-patterns 2021-11-25 16:04:44 +00:00
interactive042 [ highlighting ] case trees in :di (#2440) 2022-04-29 12:52:23 +01:00
interactive043 Add test for auto implicit case splitting. 2022-08-16 09:23:19 +02:00
interactive044 [ test ] Add a sleep 1 to the interactive044 test to work around a race condition 2022-09-04 09:17:22 +01:00
interactive045 [ test ] Fix timing issue in interactive045 test 2022-09-06 10:05:34 +01:00
interactive046 [ fix #2712 ] Don't consider CyclicMeta recoverable (#2713) 2022-10-14 14:57:55 +01:00
interface001 [ fix ] :printdef support for P(D)Pair & Equal (#2416) 2022-04-15 20:39:46 +01:00
interface002 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
interface003 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
interface004 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
interface005 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
interface006 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
interface007 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
interface008 print location of implicit name shadowing with the warning. (#1968) 2021-10-03 10:15:01 +01:00
interface009 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
interface010 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
interface011 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
interface012 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
interface013 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
interface014 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
interface015 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
interface016 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
interface017 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
interface018 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
interface019 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
interface020 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
interface021 Use Closures instead of NF in binders for normal forms (#1823) 2021-08-08 17:05:29 +01:00
interface022 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
interface023 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
interface024 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
interface025 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
interface026 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
interface027 Made unifying error msg nicer. (#1922) 2021-09-15 11:57:50 +01:00
interface028 [ parser ] bunched args in implementation implicits 2022-03-31 15:46:44 +01:00
interface029 [ new ] Handle forward declarations of implementations (#2668) 2022-09-20 21:08:50 +01:00
interpolation001 Fix #1767 2021-07-22 12:17:53 +00:00
interpolation002 Implement generic interpolation (#1967) 2021-10-13 17:26:54 +01:00
interpolation003 Implement generic interpolation (#1967) 2021-10-13 17:26:54 +01:00
interpolation004 [ fix #1626 ] Empty lines are still lines 2021-10-21 16:00:50 +01:00
interpreter001 Rename --consolewidth option to --console-width for consistency 2020-08-19 11:59:31 +01:00
interpreter002 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
interpreter003 [ refactor ] Remove Data.Strings module (#1607) 2021-06-28 13:48:37 +01:00
interpreter004 [ new ] Add Int(8/16/32/64) (#1352) 2021-05-04 08:22:06 +01:00
interpreter005 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
interpreter006 Fix REPL execExp and fix "it" (#908) 2021-01-27 23:14:41 +00:00
interpreter007 Flush standard out after writing prompt to it 2021-04-09 15:17:00 +01:00
interpreter008 Move Syntax.PreorderReasoning into base (#2368) 2022-03-22 20:58:36 +00:00
lazy001 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
lazy002 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
linear001 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
linear002 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
linear003 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
linear004 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
linear005 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
linear006 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
linear007 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
linear008 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
linear009 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
linear010 [ re #2675 ] Do not build libs/{contribs,papers} during bootstrap (#2677) 2022-10-04 13:37:45 +01:00
linear011 [ re #2675 ] Do not build libs/{contribs,papers} during bootstrap (#2677) 2022-10-04 13:37:45 +01:00
linear012 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
linear013 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
linear014 [ fix #1861 ] rewrite_impl is linear (#2150) 2021-11-25 17:07:05 +00:00
linear015 [ fix #1861 ] rewrite_impl is linear (#2150) 2021-11-25 17:07:05 +00:00
literate001 [ re #1852 ] Partial fix without the Hole UN refactoring 2021-11-24 10:54:32 +00:00
literate002 [ re #1852 ] Partial fix without the Hole UN refactoring 2021-11-24 10:54:32 +00:00
literate003 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
literate004 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
literate005 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
literate006 [ re #1852 ] Partial fix without the Hole UN refactoring 2021-11-24 10:54:32 +00:00
literate007 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
literate008 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
literate009 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
literate010 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
literate011 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
literate012 [ re #1852 ] Partial fix without the Hole UN refactoring 2021-11-24 10:54:32 +00:00
literate013 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
literate014 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
literate015 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
literate016 [ re #1852 ] Partial fix without the Hole UN refactoring 2021-11-24 10:54:32 +00:00
literate017 [ fix ] Literate things (#2312) 2022-02-18 11:29:52 +00:00
namespace001 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
namespace002 Made unifying error msg nicer. (#1922) 2021-09-15 11:57:50 +01:00
namespace003 Let qualified do-notation apply to pure and to idiom brackets (#2786) 2022-12-07 22:27:58 +00:00
params001 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
params002 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
params003 [ re #1852 ] Partial fix without the Hole UN refactoring 2021-11-24 10:54:32 +00:00
perf001 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
perf002 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
perf003 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
perf004 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
perf005 Made unifying error msg nicer. (#1922) 2021-09-15 11:57:50 +01:00
perf007 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
perf008 [ new ] Some optimisations mainly involving Nat and Fin (#1817) 2021-10-07 19:21:32 +01:00
perf009 Abandon auto search on undefined name (#1938) 2021-09-19 14:31:29 +01:00
perf010 Fix performance regression #1991 (#1995) 2021-10-11 23:53:52 +01:00
perf011 [ fix #2070 ] Look under MaybeMispelling when failing quickly 2021-10-29 17:57:55 +01:00
perf012 [ fix #2794 ] Do not ignore notinline lets in identity detection (#2795) 2022-12-06 11:41:30 +00:00
perf2202 [ fix #2202 ] Use SnocList in parser state to avoid quadratic slowdown (#2203) 2022-01-11 16:06:19 +00:00
perror001 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
perror002 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
perror003 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
perror004 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
perror005 [ cosmetic ] use the whole range when underlining the problem 2021-07-15 07:32:43 +01:00
perror006 [ cosmetic ] use the whole range when underlining the problem 2021-07-15 07:32:43 +01:00
perror007 [ new ] __LOC__, __FILE__, __LINE__, __COL__ magic debug strings (#2819) 2022-12-17 18:12:39 +00:00
perror008 noticed I was not _quite_ retaining existing behavior around Alt error processing so fixed that. updated tests. 2021-07-15 12:05:23 -07:00
perror009 Use commit to reduce the alternative parsing space as soon as an opening paren is encountered. 2021-07-14 17:22:40 -07:00
perror010 [ repl ] better printing of holes 2021-09-19 17:49:51 +01:00
perror011 [ fix #1496, fix #1345 ] propagate lex & lit fails too (#1850) 2021-08-20 16:47:47 +01:00
perror012 [ parser ] better error messages for Haskellers 2022-03-31 10:43:46 +01:00
perror013 [ syntax ] Require indent for blocks like mutual and failing (#2387) 2022-03-31 12:54:38 +01:00
perror014 [ new ] __LOC__, __FILE__, __LINE__, __COL__ magic debug strings (#2819) 2022-12-17 18:12:39 +00:00
perror015 Better parse error for missing paren after with 2022-04-29 08:59:40 +01:00
perror016 [ parser ] Make commitKeyword fail fatally 2022-09-16 11:39:53 +01:00
perror017 Add indentation checks when parsing args in implDecl 2022-09-20 23:57:54 +01:00
perror018 [ parse ] better error messages for records 2022-09-22 12:25:20 +01:00
perror019 [ parse ] Add fc to IPragma for better error messages 2022-09-25 16:09:53 +01:00
perror020 [ error ] Add FC for errors on interface constructors (#2769) 2022-11-12 22:17:42 -08:00
perror021 [ error ] Improve locality of parse errors in implicit arguments 2022-11-21 10:40:40 +00:00
perror022 [ parser ] fix issue where indentation is not checked in record parameters 2022-11-25 08:22:37 +00:00
perror023 Improve parser error messages when using reserved identifiers in decls (#2803) 2022-12-07 16:09:26 +00:00
perror024 Improve parser error messages when using reserved identifiers in decls (#2803) 2022-12-07 16:09:26 +00:00
perror025 Add mustWork in GADT data declaration parser (#2805) 2022-12-09 16:04:11 +00:00
pkg001 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
pkg002 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
pkg003 [ re #2526 ] Update golden value 2022-07-07 20:34:54 +01:00
pkg004 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
pkg005 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
pkg006 [ fix ] make color output toggling simpler and also more robust. (#2848) 2023-01-22 13:35:57 -06:00
pkg007 Fixes for processPackage (#1304) 2021-04-21 10:15:39 +01:00
pkg008 Fixes for processPackage (#1304) 2021-04-21 10:15:39 +01:00
pkg009 Fixes for processPackage (#1304) 2021-04-21 10:15:39 +01:00
pkg010 Install *.ttm on idris2 --install (#2796) 2022-12-08 21:06:17 +00:00
pkg011 Clean path in more Core.Directory functions 2022-03-23 12:49:36 +00:00
pkg012 [ new ] optional language version field to ipkg files. (#2256) 2022-01-20 10:05:53 +00:00
pkg013 Trans deps v3 (#2584) 2022-09-09 07:08:39 +01:00
pkg014 Trans deps v3 (#2584) 2022-09-09 07:08:39 +01:00
pkg015 Trans deps v3 (#2584) 2022-09-09 07:08:39 +01:00
pkg016 [ fix ] isue 2745 (#2747) 2022-11-02 12:01:19 +00:00
pkg017 [ cleanup ] ignore generated file 2022-12-12 14:47:33 +00:00
positivity001 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
positivity002 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
positivity003 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
positivity004 Use Closures instead of NF in binders for normal forms (#1823) 2021-08-08 17:05:29 +01:00
pretty001 [ new ] semantic highlighting in REPL & holes (#1836) 2021-08-13 16:00:54 +01:00
pretty002 [ fix ] Literate things (#2312) 2022-02-18 11:29:52 +00:00
primloop [ fix ] issue 2537 (#2538) 2022-07-07 09:54:52 +01:00
quantifiers001 [ base ] public export quantifier functions 2022-04-04 13:24:12 +02:00
real001 [ fix #1959 ] use modern record update syntax (#2196) 2021-12-16 18:23:18 +00:00
real002 Added seqL to Control.App and updated docs to fix #2761 2022-11-21 10:39:43 +00:00
record001 Fix performance regression #1991 (#1995) 2021-10-11 23:53:52 +01:00
record002 [ fix #1959 ] use modern record update syntax (#2196) 2021-12-16 18:23:18 +00:00
record003 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
record004 [ fix #1959 ] use modern record update syntax (#2196) 2021-12-16 18:23:18 +00:00
record005 [ fix #1959 ] use modern record update syntax (#2196) 2021-12-16 18:23:18 +00:00
record006 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
record007 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
record008 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
record009 [ fix ] elaboration of records' telescopes of parameters (#2816) 2022-12-15 17:55:50 +00:00
record010 [ fix #2002 ] implicits used in record update (#2007) 2021-10-26 17:15:29 +01:00
record011 [ fix #1959 ] use modern record update syntax (#2196) 2021-12-16 18:23:18 +00:00
record012 [ fix #2065 ] Use postfix projections if prefix ones are off (#2169) 2021-12-06 18:14:13 +00:00
record013 [ fix #1945 ] Add default support for record fields (#2175) 2021-12-06 21:21:42 +00:00
record014 [ fix ] respect totality annotations for data (#2862) 2023-01-26 11:03:22 +00:00
record015 [ fix #2176 ] Records in where-blocks are in the wrong namespace (#2187) 2022-02-16 15:43:50 +00:00
record016 [ fix ] holes in record types 2022-06-17 10:17:40 +01:00
record017 [ fix #2655 ] Add support for DataOpts in records (#2658) 2022-09-14 14:57:04 +01:00
record018 [ new ] Allow forward declarations of records 2022-10-14 14:58:29 +01:00
record019 [ re #2871 ] Fix the resolvedN issue for good 2023-02-04 16:10:47 +00:00
reflection001 [ fix #2719 ] --only behavior in Test.Golden (#2720) 2022-10-18 12:36:09 +01:00
reflection002 [ new ] semantic highlighting in REPL & holes (#1836) 2021-08-13 16:00:54 +01:00
reflection003 [ base ] Various Language.Reflection improvements (#2554) 2022-06-22 13:07:27 +01:00
reflection004 [ fix #2655 ] Add support for DataOpts in records (#2658) 2022-09-14 14:57:04 +01:00
reflection005 Made unifying error msg nicer. (#1922) 2021-09-15 11:57:50 +01:00
reflection006 print location of implicit name shadowing with the warning. (#1968) 2021-10-03 10:15:01 +01:00
reflection007 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
reflection008 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
reflection009 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
reflection010 Removed leak of internal names from test reflection010 2021-07-16 04:28:58 +02:00
reflection011 Add try primitive to reflection library (#2008) 2021-10-16 11:24:12 +01:00
reflection012 Get information about names in reflection (#2110) 2021-11-07 15:06:53 +00:00
reflection013 [ fix ] Use right reflection constructor name for unambiguing with 2021-11-23 16:42:51 +00:00
reflection014 [ fix ] elaboration of records' telescopes of parameters (#2816) 2022-12-15 17:55:50 +00:00
reflection015 [ fix ] Make able to interpret result of a macro as a function 2022-05-27 09:36:44 +01:00
reflection016 Fix an eta issue in elaborator-reflection (#2449) 2022-06-30 22:01:31 +01:00
reflection017 [ fix #2088 ] Make %runElab expression propagate its rig to check 2022-10-07 10:55:22 +02:00
reg001 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
reg002 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
reg003 [ re #1944 ] Allow toplevel aliases (#1952) 2021-10-13 21:55:23 +01:00
reg004 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
reg005 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
reg006 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
reg007 Made unifying error msg nicer. (#1922) 2021-09-15 11:57:50 +01:00
reg008 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
reg009 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
reg010 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
reg011 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
reg012 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
reg013 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
reg014 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
reg015 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
reg016 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
reg017 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
reg018 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
reg019 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
reg020 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
reg021 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
reg022 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
reg023 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
reg024 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
reg025 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
reg026 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
reg027 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
reg028 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
reg029 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
reg030 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
reg031 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
reg032 [ fix #1959 ] use modern record update syntax (#2196) 2021-12-16 18:23:18 +00:00
reg033 [ re #2001 ] Make some prelude interfaces total (#2083) 2021-11-02 15:34:52 +00:00
reg034 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
reg035 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
reg036 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
reg037 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
reg038 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
reg039 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
reg040 [ fix #2072 ] correctly handle fixity in printer 2021-11-19 17:42:07 +00:00
reg041 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
reg042 [ highlighting ] case trees in :di (#2440) 2022-04-29 12:52:23 +01:00
reg043 [ new ] put TTC files in a version-tagged directory (#2684) 2022-11-01 18:11:18 +00:00
reg044 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
reg045 Fix 'with' under implicit parameters 2021-07-14 14:51:52 +01:00
reg046 Merge branch 'unification' of https://github.com/Russoul/Idris2 into Russoul-unification 2021-07-15 20:24:27 +01:00
reg047 Add List singleton function 2021-11-05 16:08:54 +00:00
reg048 Fix display of ambiguity errors (#2075) 2021-10-30 23:08:53 +01:00
reg049 A bit of refactoring of argument elaboration order 2021-07-22 13:36:03 +01:00
reg050 Check primitives (fromInteger etc) reduce on LHS (#1903) 2021-09-05 12:37:59 +01:00
repl001 [ repl ] Add the ability to get detailed help, e.g. :help :help (#2722) 2022-10-21 14:35:33 +02:00
repl002 [ tests ] Check REPL help text and module import cmds 2022-10-13 11:31:05 +02:00
repl003 [ repl ] Add the ability to get detailed help, e.g. :help :help (#2722) 2022-10-21 14:35:33 +02:00
repl004 [ repl ] Add the ability to get detailed help, e.g. :help :help (#2722) 2022-10-21 14:35:33 +02:00
repl005 [ repl ] Add the ability to get detailed help, e.g. :help :help (#2722) 2022-10-21 14:35:33 +02:00
rewrite001 [ fix #2573 ] Solve constraints before looking at eq type 2022-07-07 20:36:05 +01:00
schemeeval001 Experimental Scheme based evaluator (#1956) 2021-09-24 20:38:55 +01:00
schemeeval002 Experimental Scheme based evaluator (#1956) 2021-09-24 20:38:55 +01:00
schemeeval003 [ highlighting ] case trees in :di (#2440) 2022-04-29 12:52:23 +01:00
schemeeval004 Experimental Scheme based evaluator (#1956) 2021-09-24 20:38:55 +01:00
schemeeval005 Fix casts in scheme evaluator (#2011) 2021-10-16 14:19:26 +01:00
schemeeval006 [ re #1987 ] test case 2021-11-25 15:12:54 +00:00
termination001 [ test ] add tricky test case ported from Agda 2022-09-02 16:06:40 +01:00
total001 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
total002 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
total003 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
total004 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
total005 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
total006 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
total007 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
total008 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
total009 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
total010 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
total011 [ re #1828 ] test case 2021-09-01 11:32:51 +01:00
total012 [ new ] put TTC files in a version-tagged directory (#2684) 2022-11-01 18:11:18 +00:00
total013 [ fix ] respect totality annotations for data (#2862) 2023-01-26 11:03:22 +00:00
total014 [ prelude ] Make some higher-kinded functions be tc-inlined 2023-01-25 16:51:11 +00:00
total015 [ fix ] respect totality annotations for data (#2862) 2023-01-26 11:03:22 +00:00
total016 [ fix ] positivity checker: assert_total & Lazy (#2876) 2023-02-07 12:35:33 +00:00
total017 [ test ] examples from termination paper 2023-02-08 16:13:04 +00:00
unification001 [ close #647 ] Already fixed (#2581) 2022-07-08 14:16:25 +01:00
warning001 print location of implicit name shadowing with the warning. (#1968) 2021-10-03 10:15:01 +01:00
warning002 [ doc ] also display definition's visibility (#2374) 2022-03-24 23:11:10 +00:00
warning003 [ fix #2229 ] better warning 2022-07-07 16:42:34 +01:00
with001 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
with002 Move rm -rf to the beginning of the test 2021-07-13 22:54:53 +01:00
with003 [ parser ] Fix issue where Alt drops incoming commit tag 2022-09-05 12:44:02 +01:00
with004 [ error ] Improve the indented non-empty block's error message 2022-03-31 10:44:06 +01:00
with005 [ base ] Add some more properties, functions and interface implementations (#2361) 2022-03-23 13:33:13 +00:00
with006 [ base ] Add some more properties, functions and interface implementations (#2361) 2022-03-23 13:33:13 +00:00
with007 [ re #499 ] quantity-aware with-clauses 2022-02-09 09:19:40 +00:00
with008 [ fix ] location information in with clauses 2022-04-01 11:41:48 +01:00
with009 [ fix ] allow refined implicit patterns in with clauses (#2393) 2022-04-03 10:45:29 +01:00
with010 [ new ] multi-with elaborated as nested withs (#2403) 2022-04-07 09:30:23 +01:00
with011 Fix at-pattern leak in recursive with blocks (#2834) 2022-12-28 09:08:09 +00:00