mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-22 11:13:36 +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.
60 lines
3.0 KiB
Plaintext
60 lines
3.0 KiB
Plaintext
1/1: Building Fld (Fld.idr)
|
|
Warning: We are about to implicitly bind the following lowercase names.
|
|
You may be unintentionally shadowing the associated global definitions:
|
|
a is shadowing Main.R1.R1.a
|
|
Warning: We are about to implicitly bind the following lowercase names.
|
|
You may be unintentionally shadowing the associated global definitions:
|
|
a is shadowing Main.R2.R2.a, Main.R1.R1.a
|
|
Warning: We are about to implicitly bind the following lowercase names.
|
|
You may be unintentionally shadowing the associated global definitions:
|
|
a is shadowing Main.R2.R2.a, Main.R1.R1.a
|
|
Warning: We are about to implicitly bind the following lowercase names.
|
|
You may be unintentionally shadowing the associated global definitions:
|
|
a is shadowing Main.R2.R2.a, Main.R1.R1.a
|
|
Warning: We are about to implicitly bind the following lowercase names.
|
|
You may be unintentionally shadowing the associated global definitions:
|
|
a is shadowing Main.R2.R2.a, Main.R1.R1.a
|
|
Warning: We are about to implicitly bind the following lowercase names.
|
|
You may be unintentionally shadowing the associated global definitions:
|
|
a is shadowing Main.R2.R2.a, Main.R1.R1.a
|
|
Warning: We are about to implicitly bind the following lowercase names.
|
|
You may be unintentionally shadowing the associated global definitions:
|
|
a is shadowing Main.R2.R2.a, Main.R1.R1.a
|
|
b is shadowing Main.Other.b
|
|
Warning: We are about to implicitly bind the following lowercase names.
|
|
You may be unintentionally shadowing the associated global definitions:
|
|
a is shadowing Main.R2.R2.a, Main.R1.R1.a
|
|
b is shadowing Main.Other.b
|
|
Warning: We are about to implicitly bind the following lowercase names.
|
|
You may be unintentionally shadowing the associated global definitions:
|
|
a is shadowing Main.R2.R2.a, Main.R1.R1.a
|
|
Warning: We are about to implicitly bind the following lowercase names.
|
|
You may be unintentionally shadowing the associated global definitions:
|
|
a is shadowing Main.R2.R2.a, Main.R1.R1.a
|
|
Warning: We are about to implicitly bind the following lowercase names.
|
|
You may be unintentionally shadowing the associated global definitions:
|
|
a is shadowing Main.R2.R2.a, Main.R1.R1.a
|
|
Warning: We are about to implicitly bind the following lowercase names.
|
|
You may be unintentionally shadowing the associated global definitions:
|
|
a is shadowing Main.R2.R2.a, Main.R1.R1.a
|
|
Warning: We are about to implicitly bind the following lowercase names.
|
|
You may be unintentionally shadowing the associated global definitions:
|
|
a is shadowing Main.R2.R2.a, Main.R1.R1.a
|
|
Error: While processing right hand side of r2_shouldNotTypecheck1. Ambiguous elaboration. Possible results:
|
|
Main.R2.MkR
|
|
Main.R1.MkR Type
|
|
|
|
Fld:72:26--72:29
|
|
68 | r1 : R1 -- explicit fields access
|
|
69 | r1 = MkR {field = "string"}
|
|
70 |
|
|
71 | r2_shouldNotTypecheck1 : ?
|
|
72 | r2_shouldNotTypecheck1 = MkR {field = the Nat 22} -- fail, impossible to disambiguate
|
|
^^^
|
|
|
|
Main> Main.myDog : OrdinaryDog
|
|
Main> Main.mySuperDog : SuperDog
|
|
Main> Main.other : Other String
|
|
Main> 1 hole: Main.r2_shouldNotTypecheck1
|
|
Main> Bye for now!
|