summaryrefslogtreecommitdiff
path: root/dhall/tests/type-errors/hurkensParadox.txt
diff options
context:
space:
mode:
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`