summaryrefslogtreecommitdiff
path: root/testdata/typesig.reject.out
diff options
context:
space:
mode:
authorPéter Diviánszky <divipp@gmail.com>2016-02-15 21:17:23 +0100
committerPéter Diviánszky <divipp@gmail.com>2016-02-15 21:17:23 +0100
commit6befbf3058a87522dc59e3e55c65a6d7b448fd9e (patch)
tree708f08e28968998b99946d58f813bb1f4773462f /testdata/typesig.reject.out
parentf29d1fc2a330b54ad57d3cb21f0f24d5714de331 (diff)
show trace only on demand
Diffstat (limited to 'testdata/typesig.reject.out')
-rw-r--r--testdata/typesig.reject.out34
1 files changed, 0 insertions, 34 deletions
diff --git a/testdata/typesig.reject.out b/testdata/typesig.reject.out
index f949fd2c..8d18a7f3 100644
--- a/testdata/typesig.reject.out
+++ b/testdata/typesig.reject.out
@@ -5,40 +5,6 @@ focus checkMetas: labEnd \{a}-><<HERE>>
5X :: 'X 5X :: 'X
6'XCase :: (b : 'X->Type) -> b X -> d:'X -> b d 6'XCase :: (b : 'X->Type) -> b X -> d:'X -> b d
7match'X :: (b : Type->Type) -> b 'X -> d:Type -> b d -> b d 7match'X :: (b : Type->Type) -> b 'X -> d:Type -> b d -> b d
8infer: labelend X : {a : _:'Type}->a
9check: ({a : _:'Type}->a :: Type) : ??
10infer: ({a : _:'Type}->a : Type) : ??
11infer: ({a : _:'Type : Type} -> a:'Type : Type) : ??
12infer: ({b : (\a:'Type -> a) : Type} -> b:'Type : Type) : ??
13focus: ({b : (\a:Type -> a) : Type} -> b:'Type : Type) : ??
14infer: ({b : \a->a : Type} -> b:'Type : Type) : ??
15focus: ({b : \a->a : Type} -> b:'Type : Type) : ??
16focus: ({b : (\a -> a:Type)} -> b:'Type : Type) : ??
17focus: ({c : (\a b:'Unit -> a)} -> c:'Type : Type) : ??
18focus: ({b : \a->a} -> b:'Type : Type) : ??
19focus: ((\a -> {b:a} -> b:'Type) : Type) : ??
20infer: ((\a -> {b:a} -> b:'Type) : Type) : ??
21check: ((\a -> {b:a} -> ('Type::Type : ??)) : Type) : ??
22infer: ((\a -> {b:a} -> ('Type:Type : ??)) : Type) : ??
23focus: ((\a -> {b:a} -> (Type:Type : ??)) : Type) : ??
24focus: ((\a -> {b:a} -> ((\c:'Unit -> Type) : ??)) : Type) : ??
25focus: ((\a -> {b:a} -> Type:??) : Type) : ??
26check: ((\a -> {b:a} -> b::Type) : Type) : ??
27infer: ((\a -> {b:a} -> b:Type) : Type) : ??
28focus: ((\a -> {b:a} -> b:Type) : Type) : ??
29focus: ((\a -> {b:a} -> \(c : Type~a)->b) : Type) : ??
30focus: ((\a -> {b:a} -> (\a:=Type -> b)) : Type) : ??
31focus: ((\a a:=Type -> {b}->b) : Type) : ??
32focus: ((\a a:=Type -> {b}->b) : Type) : ??
33focus: ({a}->a : Type) : ??
34focus: (\a:'Unit -> {b}->b) : ??
35focus: {a}->a : ??
36check: labelend X :: {a}->a
37check: labEnd (X :: {a}->a)
38check: labEnd (\{a} -> X::a)
39infer: labEnd (\{a} -> X:a)
40focus: labEnd (\{a} -> X:a)
41focus: labEnd (\{a} -> \(b : a~'X)->X)
42!focus checkMetas: labEnd \{a}-><<HERE>> 8!focus checkMetas: labEnd \{a}-><<HERE>>
43\(a : V0~'X)->X 9\(a : V0~'X)->X
44------------ tooltips 10------------ tooltips
generated by cgit v1.2.3 (git 2.39.1) at 2024-09-29 14:23:43 +0000