1
1
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-18 08:42:11 +03:00
Idris2/tests/chez/chez006/expected
Ruslan Feizerakhmanov 7aee7c9b7c
[ new ] --install-with-src; refactoring around FCs ()
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.
2021-06-05 12:53:22 +01:00

37 lines
785 B
Plaintext

1/1: Building TypeCase (TypeCase.idr)
Main> "Nat"
"List of Nat"
"List of Something else"
"List of Something else"
"List of Bool"
"Int"
"Something else"
"List of Type"
"List of Int"
43
42
Main> Main.strangeId is total
Main> Main.strangeId': strangeId' _
Main> Bye for now!
1/1: Building TypeCase2 (TypeCase2.idr)
Error: While processing left hand side of strangeId. Can't match on Nat (Erased argument).
TypeCase2:5:14--5:17
1 | data Bar = MkBar
2 | data Baz = MkBaz
3 |
4 | strangeId : a -> a
5 | strangeId {a=Nat} x = x+1
^^^
Error: While processing left hand side of foo. Can't match on Nat (Erased argument).
TypeCase2:9:5--9:8
5 | strangeId {a=Nat} x = x+1
6 | strangeId x = x
7 |
8 | foo : (0 x : Type) -> String
9 | foo Nat = "Nat"
^^^