summaryrefslogtreecommitdiff
path: root/dhall/tests/type-errors/hurkensParadox.txt
diff options
context:
space:
mode:
authorNadrieril2020-02-09 17:47:58 +0000
committerNadrieril2020-02-09 19:58:28 +0000
commit8abb6c24cd26b64d708a74faaa28cc9294dc3466 (patch)
tree836c47dbe99ed8884bf685f61315f4ce3bfc2113 /dhall/tests/type-errors/hurkensParadox.txt
parent81504a7ee24f22820c6bc85823c879d488710d11 (diff)
Move ui outputs to a sensible place
Diffstat (limited to 'dhall/tests/type-errors/hurkensParadox.txt')
-rw-r--r--dhall/tests/type-errors/hurkensParadox.txt15
1 files changed, 0 insertions, 15 deletions
diff --git a/dhall/tests/type-errors/hurkensParadox.txt b/dhall/tests/type-errors/hurkensParadox.txt
deleted file mode 100644
index 6b99615..0000000
--- a/dhall/tests/type-errors/hurkensParadox.txt
+++ /dev/null
@@ -1,15 +0,0 @@
-Type error: error: wrong type of function argument
- --> <current file>:6:23
- |
- 1 | let bottom : Type = ∀(any : Type) → any
- 2 |
- 3 | in let not : Type → Type = λ(p : Type) → p → bottom
- 4 |
-...
-10 | : pow (pow U) → U
-11 | = λ(t : pow (pow U))
- | ^^^ this expects an argument of type: Kind
- | ^ but this has type: Sort
- |
- = note: expected type `Kind`
- found type `Sort`