summaryrefslogtreecommitdiff
path: root/testdata/typesig.reject.out
diff options
context:
space:
mode:
Diffstat (limited to 'testdata/typesig.reject.out')
-rw-r--r--testdata/typesig.reject.out8
1 files changed, 4 insertions, 4 deletions
diff --git a/testdata/typesig.reject.out b/testdata/typesig.reject.out
index 7d9272bc..f6a0fd30 100644
--- a/testdata/typesig.reject.out
+++ b/testdata/typesig.reject.out
@@ -1,16 +1,16 @@
1focus checkMetas: \a -> (\b:Type -> primFix a b) (\(a:=Type) -> \c:Type -> <<HERE>>) 1focus checkMetas: \a -> (\b:Type -> primFix a b) (\(a:=Type) -> \c:Type -> <<HERE>>)
2\(a : Type~V0) (b : V1~'X) -> typeAnn V2 (labend X) 2\(a : Type~a_) (b : b_~'X) -> typeAnn c_ (labend X)
3------------ trace 3------------ trace
4'X :: Type 4'X :: Type
5X :: 'X 5X :: 'X
6'XCase :: (a : 'X->Type) -> a X -> b:'X -> a b 6'XCase :: (a : 'X->Type) -> a X -> b:'X -> a b
7match'X :: (a : Type->Type) -> a 'X -> b:Type -> a b -> a b 7match'X :: (a : Type->Type) -> a 'X -> b:Type -> a b -> a b
8!focus checkMetas: \a -> (\b:Type -> primFix a b) (\(a:=Type) -> \c:Type -> <<HERE>>) 8!focus checkMetas: \a -> (\b:Type -> primFix a b) (\(a:=Type) -> \c:Type -> <<HERE>>)
9\(a : Type~V0) (b : V1~'X) -> typeAnn V2 (labend X) 9\(a : Type~a_) (b : b_~'X) -> typeAnn c_ (labend X)
10------------ tooltips 10------------ tooltips
11testdata/typesig.reject.lc 4:6-4:7 Type 11testdata/typesig.reject.lc 4:6-4:7 Type
12testdata/typesig.reject.lc 4:6-4:11 Type 12testdata/typesig.reject.lc 4:6-4:11 Type
13testdata/typesig.reject.lc 4:10-4:11 X 13testdata/typesig.reject.lc 4:10-4:11 X
14testdata/typesig.reject.lc 6:6-6:7 V1 14testdata/typesig.reject.lc 6:6-6:7 b_
15testdata/typesig.reject.lc 6:6-7:6 V0->V1 | V2 15testdata/typesig.reject.lc 6:6-7:6 a_->b_ | c_
16testdata/typesig.reject.lc 7:5-7:6 X 16testdata/typesig.reject.lc 7:5-7:6 X