summaryrefslogtreecommitdiff
path: root/testdata/language-features/basic-list/list10.reject.out
diff options
context:
space:
mode:
Diffstat (limited to 'testdata/language-features/basic-list/list10.reject.out')
-rw-r--r--testdata/language-features/basic-list/list10.reject.out141
1 files changed, 141 insertions, 0 deletions
diff --git a/testdata/language-features/basic-list/list10.reject.out b/testdata/language-features/basic-list/list10.reject.out
index 8f1376a7..6c108119 100644
--- a/testdata/language-features/basic-list/list10.reject.out
+++ b/testdata/language-features/basic-list/list10.reject.out
@@ -4,3 +4,144 @@ with
4'Float 4'Float
5 5
6in builtin Nil 6in builtin Nil
7
8------------ trace
9infer: labelend (Cons (fromInt 1) (Cons 1.2 Nil) : 'List 'Int)
10infer: labEnd (Cons (fromInt 1) (Cons 1.2 Nil) : 'List 'Int)
11check: labEnd (('List 'Int :: Type) : ??)
12infer: labEnd (('List 'Int : Type) : ??)
13focus: labEnd (('List 'Int : Type) : ??)
14focus: labEnd ((\a:'Unit -> 'List) 'Int : ??)
15focus: labEnd ('List 'Int : ??)
16check: labEnd ('List 'Int::Type : ??)
17infer: labEnd ('List 'Int:Type : ??)
18focus: labEnd ('List 'Int:Type : ??)
19focus: labEnd ('List (\a:'Unit -> 'Int) : ??)
20focus: labEnd ('List 'Int : ??)
21focus: labEnd ('List 'Int : ??)
22check: labEnd (Cons (fromInt 1) (Cons 1.2 Nil) :: 'List 'Int)
23infer: labEnd (Cons (fromInt 1) (Cons 1.2 Nil) : 'List 'Int)
24infer: labEnd (Cons (fromInt 1) (Cons 1.2 Nil) : 'List 'Int)
25focus: labEnd (Cons (fromInt 1) (Cons 1.2 Nil) : 'List 'Int)
26focus: labEnd (Cons {_ : _:'Type} (fromInt 1) (Cons 1.2 Nil) : 'List 'Int)
27check: labEnd (Cons {(_ : _:'Type) :: Type} (fromInt 1) (Cons 1.2 Nil) : 'List 'Int)
28infer: labEnd (Cons {(_ : _:'Type) : Type} (fromInt 1) (Cons 1.2 Nil) : 'List 'Int)
29infer: labEnd (Cons {\(a : _:'Type)->a : Type} (fromInt 1) (Cons 1.2 Nil) : 'List 'Int)
30infer: labEnd (Cons {\(b : (\a:'Type -> a))->b : Type} (fromInt 1) (Cons 1.2 Nil) : 'List 'Int)
31focus: labEnd (Cons {\(b : (\a:Type -> a))->b : Type} (fromInt 1) (Cons 1.2 Nil) : 'List 'Int)
32infer: labEnd (Cons {\(b : \a->a)->b : Type} (fromInt 1) (Cons 1.2 Nil) : 'List 'Int)
33focus: labEnd (Cons {\(b : \a->a)->b : Type} (fromInt 1) (Cons 1.2 Nil) : 'List 'Int)
34focus: labEnd (Cons {(\a b:a -> b) : Type} (fromInt 1) (Cons 1.2 Nil) : 'List 'Int)
35infer: labEnd (Cons {(\a b:a -> b) : Type} (fromInt 1) (Cons 1.2 Nil) : 'List 'Int)
36focus: labEnd (Cons {(\a b:a -> b) : Type} (fromInt 1) (Cons 1.2 Nil) : 'List 'Int)
37focus: labEnd (Cons {\a b:a -> b:Type} (fromInt 1) (Cons 1.2 Nil) : 'List 'Int)
38focus: labEnd (Cons {\a b:a -> \(c : Type~a)->b} (fromInt 1) (Cons 1.2 Nil) : 'List 'Int)
39focus: labEnd (Cons {\a b:a a:=Type -> b} (fromInt 1) (Cons 1.2 Nil) : 'List 'Int)
40focus: labEnd (Cons {\a a:=Type -> \b->b} (fromInt 1) (Cons 1.2 Nil) : 'List 'Int)
41focus: labEnd (Cons {\a->a} (fromInt 1) (Cons 1.2 Nil) : 'List 'Int)
42focus: labEnd ((\a -> Cons {a}) (fromInt 1) (Cons 1.2 Nil) : 'List 'Int)
43focus: labEnd (\a->Cons (fromInt 1) (Cons 1.2 Nil) : 'List 'Int)
44focus: labEnd ((\a -> Cons (fromInt 1)) (Cons 1.2 Nil) : 'List 'Int)
45check: labEnd ((\a -> Cons (fromInt 1 :: a)) (Cons 1.2 Nil) : 'List 'Int)
46infer: labEnd ((\a -> Cons (fromInt 1 : a)) (Cons 1.2 Nil) : 'List 'Int)
47focus: labEnd ((\a -> Cons (fromInt 1 : a)) (Cons 1.2 Nil) : 'List 'Int)
48focus: labEnd ((\a -> Cons (fromInt 1 : a)) (Cons 1.2 Nil) : 'List 'Int)
49focus: labEnd ((\a -> Cons (fromInt {_ : _:'Type} 1 : a)) (Cons 1.2 Nil) : 'List 'Int)
50check: labEnd ((\a -> Cons (fromInt {(_ : _:'Type) :: Type} 1 : a)) (Cons 1.2 Nil) : 'List 'Int)
51infer: labEnd ((\a -> Cons (fromInt {(_ : _:'Type) : Type} 1 : a)) (Cons 1.2 Nil) : 'List 'Int)
52infer: labEnd ((\a -> Cons (fromInt {\(b : _:'Type)->b : Type} 1 : a)) (Cons 1.2 Nil) : 'List 'Int)
53infer: labEnd ((\a -> Cons (fromInt {\(c : (\b:'Type -> b))->c : Type} 1 : a)) (Cons 1.2 Nil) : 'List 'Int)
54focus: labEnd ((\a -> Cons (fromInt {\(c : (\b:Type -> b))->c : Type} 1 : a)) (Cons 1.2 Nil) : 'List 'Int)
55infer: labEnd ((\a -> Cons (fromInt {\(c : \b->b)->c : Type} 1 : a)) (Cons 1.2 Nil) : 'List 'Int)
56focus: labEnd ((\a -> Cons (fromInt {\(c : \b->b)->c : Type} 1 : a)) (Cons 1.2 Nil) : 'List 'Int)
57focus: labEnd ((\a -> Cons (fromInt {(\b c:b -> c) : Type} 1 : a)) (Cons 1.2 Nil) : 'List 'Int)
58infer: labEnd ((\a -> Cons (fromInt {(\b c:b -> c) : Type} 1 : a)) (Cons 1.2 Nil) : 'List 'Int)
59focus: labEnd ((\a -> Cons (fromInt {(\b c:b -> c) : Type} 1 : a)) (Cons 1.2 Nil) : 'List 'Int)
60focus: labEnd ((\a -> Cons (fromInt {\b c:b -> c:Type} 1 : a)) (Cons 1.2 Nil) : 'List 'Int)
61focus: labEnd ((\a -> Cons (fromInt {\b c:b -> \(d : Type~b)->c} 1 : a)) (Cons 1.2 Nil) : 'List 'Int)
62focus: labEnd ((\a -> Cons (fromInt {\b c:b b:=Type -> c} 1 : a)) (Cons 1.2 Nil) : 'List 'Int)
63focus: labEnd ((\a -> Cons (fromInt {\b b:=Type -> \c->c} 1 : a)) (Cons 1.2 Nil) : 'List 'Int)
64focus: labEnd ((\a -> Cons (fromInt {\b->b} 1 : a)) (Cons 1.2 Nil) : 'List 'Int)
65focus: labEnd ((\a -> Cons ((\b -> fromInt {b}) 1 : a)) (Cons 1.2 Nil) : 'List 'Int)
66focus: labEnd ((\a -> Cons ((\b -> fromInt b) 1 : a)) (Cons 1.2 Nil) : 'List 'Int)
67focus: labEnd ((\a -> Cons ((\b -> fromInt b 1) : a)) (Cons 1.2 Nil) : 'List 'Int)
68focus: labEnd ((\a -> Cons ((\b -> fromInt b {_ : _:'Type} 1) : a)) (Cons 1.2 Nil) : 'List 'Int)
69check: labEnd ((\a -> Cons ((\b -> fromInt b {(_ : _:'Type) :: 'Num b} 1) : a)) (Cons 1.2 Nil) : 'List 'Int)
70infer: labEnd ((\a -> Cons ((\b -> fromInt b {(_ : _:'Type) : 'Num b} 1) : a)) (Cons 1.2 Nil) : 'List 'Int)
71infer: labEnd ((\a -> Cons ((\b -> fromInt b {\(c : _:'Type)->c : 'Num b} 1) : a)) (Cons 1.2 Nil) : 'List 'Int)
72infer: labEnd ((\a -> Cons ((\b -> fromInt b {\(d : (\c:'Type -> c))->d : 'Num b} 1) : a)) (Cons 1.2 Nil) : 'List 'Int)
73focus: labEnd ((\a -> Cons ((\b -> fromInt b {\(d : (\c:Type -> c))->d : 'Num b} 1) : a)) (Cons 1.2 Nil) : 'List 'Int)
74infer: labEnd ((\a -> Cons ((\b -> fromInt b {\(d : \c->c)->d : 'Num b} 1) : a)) (Cons 1.2 Nil) : 'List 'Int)
75focus: labEnd ((\a -> Cons ((\b -> fromInt b {\(d : \c->c)->d : 'Num b} 1) : a)) (Cons 1.2 Nil) : 'List 'Int)
76focus: labEnd ((\a -> Cons ((\b -> fromInt b {(\c d:c -> d) : 'Num b} 1) : a)) (Cons 1.2 Nil) : 'List 'Int)
77infer: labEnd ((\a -> Cons ((\b -> fromInt b {(\c d:c -> d) : 'Num b} 1) : a)) (Cons 1.2 Nil) : 'List 'Int)
78focus: labEnd ((\a -> Cons ((\b -> fromInt b {(\c d:c -> d) : 'Num b} 1) : a)) (Cons 1.2 Nil) : 'List 'Int)
79focus: labEnd ((\a -> Cons ((\b -> fromInt b {\c d:c -> d : 'Num b} 1) : a)) (Cons 1.2 Nil) : 'List 'Int)
80focus: labEnd ((\a -> Cons ((\b -> fromInt b {\c d:c -> \(e : 'Num b ~ c)->d} 1) : a)) (Cons 1.2 Nil) : 'List 'Int)
81focus: labEnd ((\a -> Cons ((\b -> fromInt b {\c d:c -> \(c := 'Num b)->d} 1) : a)) (Cons 1.2 Nil) : 'List 'Int)
82focus: labEnd ((\a -> Cons ((\b -> fromInt b {\c (c := 'Num b) -> \(d : 'Num b)->d} 1) : a)) (Cons 1.2 Nil) : 'List 'Int)
83focus: labEnd ((\a -> Cons ((\b -> fromInt b {\(c : 'Num b)->c} 1) : a)) (Cons 1.2 Nil) : 'List 'Int)
84focus: labEnd ((\a -> Cons ((\b -> (\(c : 'Num b) -> fromInt b {c}) 1) : a)) (Cons 1.2 Nil) : 'List 'Int)
85focus: labEnd ((\a -> Cons ((\b -> (\(c : 'Num b) -> fromInt b c) 1) : a)) (Cons 1.2 Nil) : 'List 'Int)
86focus: labEnd ((\a -> Cons ((\b (c : 'Num b) -> fromInt b c 1) : a)) (Cons 1.2 Nil) : 'List 'Int)
87check: labEnd ((\a -> Cons ((\b (c : 'Num b) -> fromInt b c 1::'Int) : a)) (Cons 1.2 Nil) : 'List 'Int)
88infer: labEnd ((\a -> Cons ((\b (c : 'Num b) -> fromInt b c 1:'Int) : a)) (Cons 1.2 Nil) : 'List 'Int)
89focus: labEnd ((\a -> Cons ((\b (c : 'Num b) -> fromInt b c 1:'Int) : a)) (Cons 1.2 Nil) : 'List 'Int)
90focus: labEnd ((\a -> Cons ((\b (c : 'Num b) -> fromInt b c (\d:'Unit -> 1)) : a)) (Cons 1.2 Nil) : 'List 'Int)
91focus: labEnd ((\a -> Cons ((\b (c : 'Num b) -> fromInt b c 1) : a)) (Cons 1.2 Nil) : 'List 'Int)
92focus: labEnd ((\a -> Cons ((\b (c : 'Num b) -> fromInt b c 1) : a)) (Cons 1.2 Nil) : 'List 'Int)
93focus: labEnd ((\a -> Cons (\b (c : 'Num b) -> fromInt b c 1 : a)) (Cons 1.2 Nil) : 'List 'Int)
94focus: labEnd ((\a -> Cons (\b (c : 'Num b) (d : a~b) -> fromInt b c 1)) (Cons 1.2 Nil) : 'List 'Int)
95focus: labEnd ((\a -> Cons (\b (c : 'Num b) b:=a -> fromInt a c 1)) (Cons 1.2 Nil) : 'List 'Int)
96focus: labEnd ((\a -> Cons (\b b:=a (c : 'Num a) -> fromInt a c 1)) (Cons 1.2 Nil) : 'List 'Int)
97focus: labEnd ((\a -> Cons (\(b : 'Num a) -> fromInt a b 1)) (Cons 1.2 Nil) : 'List 'Int)
98focus: labEnd ((\a (b : 'Num a) -> Cons (fromInt a b 1)) (Cons 1.2 Nil) : 'List 'Int)
99focus: labEnd ((\a (b : 'Num a) -> Cons (fromInt a b 1)) (Cons 1.2 Nil) : 'List 'Int)
100focus: labEnd (\a (b : 'Num a) -> Cons (fromInt a b 1) (Cons 1.2 Nil) : 'List 'Int)
101focus: labEnd (\a (b : 'Num a) -> (\(c : 'Int~a) -> Cons (fromInt a b 1)) (Cons 1.2 Nil))
102focus: labEnd (\a (b : 'Num a) -> (\a:='Int -> Cons 1) (Cons 1.2 Nil))
103focus: labEnd (\a (b : 'Num a) a:='Int -> Cons 1 (Cons 1.2 Nil))
104check: labEnd (\a (b : 'Num a) a:='Int -> Cons 1 (Cons 1.2 Nil :: 'List 'Int))
105infer: labEnd (\a (b : 'Num a) a:='Int -> Cons 1 (Cons 1.2 Nil : 'List 'Int))
106infer: labEnd (\a (b : 'Num a) a:='Int -> Cons 1 (Cons 1.2 Nil : 'List 'Int))
107focus: labEnd (\a (b : 'Num a) a:='Int -> Cons 1 (Cons 1.2 Nil : 'List 'Int))
108focus: labEnd (\a (b : 'Num a) a:='Int -> Cons 1 (Cons {_ : _:'Type} 1.2 Nil : 'List 'Int))
109check: labEnd (\a (b : 'Num a) a:='Int -> Cons 1 (Cons {(_ : _:'Type) :: Type} 1.2 Nil : 'List 'Int))
110infer: labEnd (\a (b : 'Num a) a:='Int -> Cons 1 (Cons {(_ : _:'Type) : Type} 1.2 Nil : 'List 'Int))
111infer: labEnd (\a (b : 'Num a) a:='Int -> Cons 1 (Cons {\(c : _:'Type)->c : Type} 1.2 Nil : 'List 'Int))
112infer: labEnd (\a (b : 'Num a) a:='Int -> Cons 1 (Cons {\(d : (\c:'Type -> c))->d : Type} 1.2 Nil : 'List 'Int))
113focus: labEnd (\a (b : 'Num a) a:='Int -> Cons 1 (Cons {\(d : (\c:Type -> c))->d : Type} 1.2 Nil : 'List 'Int))
114infer: labEnd (\a (b : 'Num a) a:='Int -> Cons 1 (Cons {\(d : \c->c)->d : Type} 1.2 Nil : 'List 'Int))
115focus: labEnd (\a (b : 'Num a) a:='Int -> Cons 1 (Cons {\(d : \c->c)->d : Type} 1.2 Nil : 'List 'Int))
116focus: labEnd (\a (b : 'Num a) a:='Int -> Cons 1 (Cons {(\c d:c -> d) : Type} 1.2 Nil : 'List 'Int))
117infer: labEnd (\a (b : 'Num a) a:='Int -> Cons 1 (Cons {(\c d:c -> d) : Type} 1.2 Nil : 'List 'Int))
118focus: labEnd (\a (b : 'Num a) a:='Int -> Cons 1 (Cons {(\c d:c -> d) : Type} 1.2 Nil : 'List 'Int))
119focus: labEnd (\a (b : 'Num a) a:='Int -> Cons 1 (Cons {\c d:c -> d:Type} 1.2 Nil : 'List 'Int))
120focus: labEnd (\a (b : 'Num a) a:='Int -> Cons 1 (Cons {\c d:c -> \(e : Type~c)->d} 1.2 Nil : 'List 'Int))
121focus: labEnd (\a (b : 'Num a) a:='Int -> Cons 1 (Cons {\c d:c c:=Type -> d} 1.2 Nil : 'List 'Int))
122focus: labEnd (\a (b : 'Num a) a:='Int -> Cons 1 (Cons {\c c:=Type -> \d->d} 1.2 Nil : 'List 'Int))
123focus: labEnd (\a (b : 'Num a) a:='Int -> Cons 1 (Cons {\c->c} 1.2 Nil : 'List 'Int))
124focus: labEnd (\a (b : 'Num a) a:='Int -> Cons 1 ((\c -> Cons {c}) 1.2 Nil : 'List 'Int))
125focus: labEnd (\a (b : 'Num a) a:='Int -> Cons 1 (\c->Cons 1.2 Nil : 'List 'Int))
126focus: labEnd (\a (b : 'Num a) a:='Int -> Cons 1 ((\c -> Cons 1.2) Nil : 'List 'Int))
127check: labEnd (\a (b : 'Num a) a:='Int -> Cons 1 ((\c -> Cons 1.2::c) Nil : 'List 'Int))
128infer: labEnd (\a (b : 'Num a) a:='Int -> Cons 1 ((\c -> Cons 1.2:c) Nil : 'List 'Int))
129focus: labEnd (\a (b : 'Num a) a:='Int -> Cons 1 ((\c -> Cons 1.2:c) Nil : 'List 'Int))
130focus: labEnd (\a (b : 'Num a) a:='Int -> Cons 1 ((\c -> Cons \(d : c~'Float)->1.2) Nil : 'List 'Int))
131focus: labEnd (\a (b : 'Num a) a:='Int -> Cons 1 ((\c -> Cons (\c:='Float -> 1.2)) Nil : 'List 'Int))
132focus: labEnd (\a (b : 'Num a) a:='Int -> Cons 1 ((\c c:='Float -> Cons 1.2) Nil : 'List 'Int))
133focus: labEnd (\a (b : 'Num a) a:='Int -> Cons 1 ((\c c:='Float -> Cons 1.2) Nil : 'List 'Int))
134focus: labEnd (\a (b : 'Num a) a:='Int -> Cons 1 (Cons 1.2 Nil : 'List 'Int))
135focus: labEnd (\a (b : 'Num a) a:='Int -> Cons 1 ((\(c : 'Empty "can not unify\n\ESC[32m'Int\ESC[m\nwith\n\ESC[32m'Float\ESC[m\n") -> Cons 1.2) Nil))
136!type error: can not unify
137'Int
138with
139'Float
140
141in builtin Nil
142
143------------ tooltips
144testdata/language-features/basic-list/list10.reject.lc 1:10-1:11 V1
145testdata/language-features/basic-list/list10.reject.lc 1:12-1:15 Float
146testdata/language-features/basic-list/list10.reject.lc 1:20-1:25 Type
147testdata/language-features/basic-list/list10.reject.lc 1:21-1:24 Type
generated by cgit v1.2.3 (git 2.39.1) at 2024-09-29 22:40:17 +0000