mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-17 00:10:31 +03:00
7aee7c9b7c
Why: * To implement robust cross-project go-to-definition in LSP i.e you can jump to definition of any global name coming from library dependencies, as well as from the local project files. What it does: * Modify `FC`s to carry `ModuleIdent` for .idr sources, file name for .ipkg sources or nothing for interactive runs. * Add `--install-with-src` to install the source code alongside the ttc binaries. The source is installed into the same directory as the corresponding ttc file. Installed sources are made read-only. * As we install the sources pinned to the related ttc files we gain the versioning of sources for free.
62 lines
1.5 KiB
Plaintext
62 lines
1.5 KiB
Plaintext
1/1: Building Issue1169 (Issue1169.idr)
|
|
Error: test is not covering.
|
|
|
|
Issue1169:3:1--3:26
|
|
1 | %default total
|
|
2 |
|
|
3 | test : (String, ()) -> ()
|
|
^^^^^^^^^^^^^^^^^^^^^^^^^
|
|
|
|
Missing cases:
|
|
test (_, _)
|
|
|
|
Error: test' is not covering.
|
|
|
|
Issue1169:6:1--6:24
|
|
2 |
|
|
3 | test : (String, ()) -> ()
|
|
4 | test ("a", ()) = ()
|
|
5 |
|
|
6 | test' : (Int, ()) -> ()
|
|
^^^^^^^^^^^^^^^^^^^^^^^
|
|
|
|
Missing cases:
|
|
test' (_, _)
|
|
|
|
Error: test'' is not covering.
|
|
|
|
Issue1169:9:1--9:22
|
|
5 |
|
|
6 | test' : (Int, ()) -> ()
|
|
7 | test' (1, ()) = ()
|
|
8 |
|
|
9 | test'' : Type -> Type
|
|
^^^^^^^^^^^^^^^^^^^^^
|
|
|
|
Missing cases:
|
|
test'' _
|
|
|
|
1/1: Building Issue1366 (Issue1366.idr)
|
|
Warning: We are about to implicitly bind the following lowercase names.
|
|
You may be unintentionally shadowing the associated global definitions:
|
|
f is shadowing Main.f
|
|
Warning: We are about to implicitly bind the following lowercase names.
|
|
You may be unintentionally shadowing the associated global definitions:
|
|
f is shadowing Main.f
|
|
Warning: We are about to implicitly bind the following lowercase names.
|
|
You may be unintentionally shadowing the associated global definitions:
|
|
f is shadowing Main.f
|
|
Error: decode is not covering.
|
|
|
|
Issue1366:33:1--33:45
|
|
29 | data Funny : (a : Type) -> (f : Type -> Type) -> Type where
|
|
30 | A : List a -> f a -> Funny a f
|
|
31 | B : Funny a f
|
|
32 |
|
|
33 | decode : NS [[List a, f a], []] -> Funny a f
|
|
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
|
|
|
|
Missing cases:
|
|
decode (S _)
|
|
|