From 130de8cea49c848a06174c61c747d9414a5c71b7 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sun, 16 Feb 2020 19:06:23 +0000
Subject: Start requiring Universe to build a Type

---
 tests_buffer | 1 +
 1 file changed, 1 insertion(+)

(limited to 'tests_buffer')

diff --git a/tests_buffer b/tests_buffer
index e8eb3d7..1c814ff 100644
--- a/tests_buffer
+++ b/tests_buffer
@@ -52,6 +52,7 @@ success/
             (λ(T : Type) → let x = 0 in λ(x : T) → x) : ∀(T : Type) → ∀(x : T) → T
 failure/
     \(_: Bool) -> assert : (\(_: Bool) -> _) === (\(x: Bool) -> _)
+    unit/FunctionTypeOutputTypeNotAType Bool -> 1
     merge { x = λ(x : Bool) → x } (< x: Bool | y: Natural >.x True)
     merge { x = λ(_ : Bool) → _, y = 1 } < x = True | y >
     merge { x = True, y = 1 } < x | y >.x
-- 
cgit v1.2.3