git.iko.soy/Idris-dev
on 385dcbf help sign in
Idris-dev/test/regression002/expected
149 lines 5.6 kB history raw
1reg003a.idr:4:11:When checking type of Main.ECons:
2No such variable OddList
3reg003a.idr:7:11:When checking type of Main.OCons:
4No such variable EvenList
5reg003a.idr:9:6:When checking type of Main.test:
6No such variable EvenList
7reg006.idr:17:1:
8RBTree.lookup is possibly not total due to recursive path RBTree.lookup --> RBTree.lookup
9reg007.lidr:8:3:A.n is already defined
10reg007.lidr:12:13-19:When checking right hand side of hurrah with expected type
11 0 = 1
13Type mismatch between
14 n = lala (Type of isSame)
15and
16 0 = 1 (Expected type)
18Specifically:
19 Type mismatch between
20 1
21 and
22 0
23reg010.idr:5:15:
24When checking left hand side of with block in usubst.unsafeSubst:
25Can't match on with block in usubst.unsafeSubst warg a P x x px
26reg018a.idr:16:1:
27conat.minusCoNat is possibly not total due to recursive path conat.minusCoNat --> conat.minusCoNat
28reg018a.idr:21:1:
29conat.loopForever is possibly not total due to: conat.minusCoNat
30reg018b.idr:8:1:
31A.showB is possibly not total due to recursive path A.showB --> A.showB
32reg018b.idr:11:1:
33A.B implementation of Prelude.Show.Show is possibly not total due to: A.showB
34reg018c.idr:21:1:
35CodataTest.inf is possibly not total due to: with block in CodataTest.inf
36reg018d.idr:8:1:Main.pull is not total as there are missing cases
37reg023.idr:7:5:When checking right hand side of bad with expected type
38 f Nat
40Type mismatch between
41 Nat (Type of 0)
42and
43 f Nat (Expected type)
44reg028.idr:5:1:tbad.bad is possibly not total due to: with block in tbad.bad
45reg028a.idr:17:14-19:
46This style of tactic proof is deprecated. See %runElab for the replacement.
47reg028a.idr:11:1:
48tbad.qsort' is possibly not total due to: with block in tbad.qsort'
49reg034.idr:6:5:When checking left hand side of bar:
50Can't match on bar xs xs Refl
51reg034.idr:9:5:When checking left hand side of foo:
52Can't match on foo f x x Refl
53reg035b.idr:8:6:No such variable __pi_arg
54reg044.idr:4:6-11:
55This style of tactic proof is deprecated. See %runElab for the replacement.
56reg044.idr:4:4:When checking right hand side of Main.pf with expected type
57 (b : Nat) -> (a : Nat) -> (S a = S b) -> a = b
59Type mismatch between
60 b = b (Type of Refl)
61and
62 a = b (Expected type)
64Specifically:
65 Type mismatch between
66 b
67 and
68 a
69reg049.idr:2:9:When checking constructor Main.Bogus:
70Void is not Main.Foo
71reg049.idr:5:6:When checking right hand side of uhOh with expected type
72 Void
74No such variable Bogus
75./badbangop.idr:7:1: error: ! is
76 not a valid
77 operator, expected: space
78(!) : List a -> Nat -> Maybe a
79^
80./baddoublebang.idr:6:28: error: unexpected
81 Operator without known fixity:
82 !!, expected: space
83doubleBang mmn = do pure !!mmn
84 ^
85reg054.idr:18:5:When checking left hand side of inf:
86When checking an application of constructor Main.MkInfer:
87 Attempting concrete match on polymorphic argument: 0
88reg054.idr:34:7:When checking left hand side of weird:
89No explicit types on left hand side: Char
90reg054.idr:37:8:When checking left hand side of weird':
91No explicit types on left hand side: Nat
92reg054.idr:40:1-8:When checking left hand side of tctrick:
93When checking an application of Main.tctrick:
94 Type mismatch between
95 Maybe a1 (Type of Just x)
96 and
97 a (Expected type)
98reg055.idr:5:3:When checking left hand side of g:
99Can't match on g (f 0)
100reg055.idr:8:3:When checking left hand side of h:
101Can't match on h x x
102reg055a.idr:8:5:When checking left hand side of foo:
103When checking an application of constructor Foo.CAny:
104 Attempting concrete match on polymorphic argument: Nothing
105reg055a.idr:13:7:When checking left hand side of Foo.apply:
106Can't match on apply (\x, y => x) a
107reg056.idr:7:7:dodgy n m Refl is a valid case
108reg056.idr:10:6:nonk Refl is a valid case
109reg068.idr:1:6:Main.nat has a name which may be implicitly bound.
110This is likely to lead to problems!
111reg068.idr:2:6:Main.ze has a name which may be implicitly bound.
112This is likely to lead to problems!
113reg068.idr:2:8-11:WARNING: nat is bound as an implicit
114 Did you mean to refer to Main.nat?
115reg068.idr:2:6:When checking constructor Main.ze:
116Type level variable nat is not Main.nat
117Mod.idr:11:1:public export Mod.natexp can't refer to export Mod.natfn
118reg070.idr:7:1:
119Test_show.Te implementation of Prelude.Show.Show is possibly not total due to: Prelude.Show.Test_show.Te implementation of Prelude.Show.Show, method show
120./reg076.idr:8:1: error: Missing
121 fixity declaration for
122 Main.:>, expected: "->", "=>",
123 ambiguous use of a left-associative operator,
124 ambiguous use of a non-associative operator,
125 ambiguous use of a right-associative operator
126<EOF>
127^
128./reg077.idr:3:1: error: Missing
129 fixity declaration for
130 Main.:>>, expected: ")", ";",
131 "in", start of block
132<EOF>
133^
134DoubleEquality.idr:4:87:When checking right hand side of oops with expected type
135 Void
137When checking argument value to function Prelude.Basics.the:
138 Type mismatch between
139 x = x (Type of Refl)
140 and
141 (-0.0) = 0.0 (Expected type)
143 Specifically:
144 Type mismatch between
145 -0.0
146 and
147 0.0
148Canonicity.idr:9:1:Canonicity.f is not total as there are missing cases
149Canonicity.idr:12:1:Canonicity.NaN is possibly not total due to: Canonicity.f