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.
22 lines
626 B
Plaintext
22 lines
626 B
Plaintext
1/1: Building eq (eq.idr)
|
|
Error: badeq x y p is not a valid impossible case.
|
|
|
|
eq:27:1--27:23
|
|
23 | eqL2 : (xs : List a) -> (x :: xs = x :: y :: xs) -> Nat
|
|
24 | eqL2 xs p impossible
|
|
25 |
|
|
26 | badeq : (x : Nat) -> (y : Nat) -> (S (S x) = S y) -> Nat
|
|
27 | badeq x y p impossible
|
|
^^^^^^^^^^^^^^^^^^^^^^
|
|
|
|
Error: badeqL xs ys p is not a valid impossible case.
|
|
|
|
eq:30:1--30:26
|
|
26 | badeq : (x : Nat) -> (y : Nat) -> (S (S x) = S y) -> Nat
|
|
27 | badeq x y p impossible
|
|
28 |
|
|
29 | badeqL : (xs : List a) -> (ys : List a) -> (x :: xs = x :: y :: ys) -> Nat
|
|
30 | badeqL xs ys p impossible
|
|
^^^^^^^^^^^^^^^^^^^^^^^^^
|
|
|