mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-09-21 14:09:30 +03:00
Don't let tests depend on colouring.
This commit is contained in:
parent
663c401154
commit
8cc2312715
@ -1,4 +1,4 @@
|
||||
DefaultArgUnknownName.idr:9:6:
|
||||
When elaborating right hand side of test:
|
||||
When elaborating argument [95marg[0m to function [92mDefaultArgUnknownName.funWithBadDefArg[0m:
|
||||
When elaborating argument arg to function DefaultArgUnknownName.funWithBadDefArg:
|
||||
No such variable sadgjhsag
|
||||
|
@ -1,3 +1,3 @@
|
||||
#!/usr/bin/env bash
|
||||
idris --consolewidth 80 --check $@ DefaultArgUnknownName.idr
|
||||
idris --nocolour --consolewidth 80 --check $@ DefaultArgUnknownName.idr
|
||||
rm -f *.ibc
|
||||
|
@ -1,5 +1,5 @@
|
||||
reg023.idr:7:5:When elaborating right hand side of bad:
|
||||
Can't unify
|
||||
[94mNat[0m (Type of [91m0[0m)
|
||||
Nat (Type of 0)
|
||||
with
|
||||
[92mf[0m [94mNat[0m (Expected type)
|
||||
f Nat (Expected type)
|
||||
|
@ -1,3 +1,3 @@
|
||||
#!/usr/bin/env bash
|
||||
idris --consolewidth 80 $@ reg023.idr --check
|
||||
idris --nocolour --consolewidth 80 $@ reg023.idr --check
|
||||
rm -f *.ibc
|
||||
|
@ -1,4 +1,4 @@
|
||||
reg034.idr:6:5:When elaborating left hand side of bar:
|
||||
Can't match on bar xs xs [91mRefl[0m
|
||||
Can't match on bar xs xs Refl
|
||||
reg034.idr:9:5:When elaborating left hand side of foo:
|
||||
Can't match on foo f x x [91mRefl[0m
|
||||
Can't match on foo f x x Refl
|
||||
|
@ -1,3 +1,3 @@
|
||||
#!/usr/bin/env bash
|
||||
idris --consolewidth 80 --check reg034.idr
|
||||
idris --nocolour --consolewidth 80 --check reg034.idr
|
||||
rm -f reg034 *.ibc
|
||||
|
@ -1,4 +1,4 @@
|
||||
reg035b.idr:8:6:Can't convert
|
||||
[94mAdditive[0m -> [94mNat[0m
|
||||
Additive -> Nat
|
||||
with
|
||||
[94mFin[0m [91m0[0m
|
||||
Fin 0
|
||||
|
@ -1,5 +1,5 @@
|
||||
#!/usr/bin/env bash
|
||||
idris --consolewidth 80 --check reg035.idr
|
||||
idris --consolewidth 80 --check reg035a.lidr
|
||||
idris --consolewidth 80 --check reg035b.idr
|
||||
idris --nocolour --consolewidth 80 --check reg035.idr
|
||||
idris --nocolour --consolewidth 80 --check reg035a.lidr
|
||||
idris --nocolour --consolewidth 80 --check reg035b.idr
|
||||
rm -f *.ibc
|
||||
|
@ -1,11 +1,11 @@
|
||||
reg044.idr:4:4:When elaborating right hand side of Main.pf:
|
||||
Can't unify
|
||||
[95mb[0m [94m=[0m [95mb[0m (Type of [91mRefl[0m)
|
||||
b = b (Type of Refl)
|
||||
with
|
||||
[95ma[0m [94m=[0m [95mb[0m (Expected type)
|
||||
a = b (Expected type)
|
||||
|
||||
Specifically:
|
||||
Can't unify
|
||||
[95mb[0m
|
||||
b
|
||||
with
|
||||
[95ma[0m
|
||||
a
|
||||
|
@ -1,3 +1,3 @@
|
||||
#!/usr/bin/env bash
|
||||
idris --consolewidth 80 reg044.idr --check
|
||||
idris --nocolour --consolewidth 80 reg044.idr --check
|
||||
rm -f *.ibc
|
||||
|
@ -1,10 +1,10 @@
|
||||
reg054.idr:18:5:When elaborating left hand side of inf:
|
||||
When elaborating an application of constructor [91mMain.MkInfer[0m:
|
||||
When elaborating an application of constructor Main.MkInfer:
|
||||
Attempting concrete match on polymorphic argument: 0
|
||||
reg054.idr:34:7:When elaborating left hand side of weird:
|
||||
When elaborating argument [95mx[0m to Main.weird:
|
||||
When elaborating argument x to Main.weird:
|
||||
No explicit types on left hand side: Char
|
||||
reg054.idr:37:9:Can't convert
|
||||
[94mMaybe[0m a1
|
||||
Maybe a1
|
||||
with
|
||||
[95ma[0m
|
||||
a
|
||||
|
@ -1,2 +1,2 @@
|
||||
#!/usr/bin/env bash
|
||||
idris --consolewidth 80 $@ reg054.idr --check
|
||||
idris --nocolour --consolewidth 80 $@ reg054.idr --check
|
||||
|
@ -1,9 +1,9 @@
|
||||
reg055.idr:5:3:When elaborating left hand side of g:
|
||||
Can't match on g ([92mf[0m [91m0[0m)
|
||||
Can't match on g (f 0)
|
||||
reg055.idr:8:3:When elaborating left hand side of h:
|
||||
Can't match on h x x
|
||||
reg055a.idr:8:5:When elaborating left hand side of foo:
|
||||
When elaborating an application of constructor [91mFoo.CAny[0m:
|
||||
When elaborating an application of constructor Foo.CAny:
|
||||
Attempting concrete match on polymorphic argument: Nothing
|
||||
reg055a.idr:13:7:When elaborating left hand side of Foo.apply:
|
||||
Can't match on apply (\[95mx[0m => \[95my[0m => [95mx[0m) a
|
||||
Can't match on apply (\x => \y => x) a
|
||||
|
@ -1,5 +1,5 @@
|
||||
#!/usr/bin/env bash
|
||||
idris --consolewidth 80 $@ reg055.idr --check
|
||||
idris --consolewidth 80 $@ reg055a.idr --check
|
||||
idris --nocolour --consolewidth 80 $@ reg055.idr --check
|
||||
idris --nocolour --consolewidth 80 $@ reg055a.idr --check
|
||||
rm -f *.ibc
|
||||
|
||||
|
@ -1,24 +1,24 @@
|
||||
tutorial006a.idr:5:23:When elaborating right hand side of vapp:
|
||||
When elaborating argument [95mxs[0m to constructor [91mData.VectType.Vect.::[0m:
|
||||
When elaborating argument xs to constructor Data.VectType.Vect.:::
|
||||
Can't unify
|
||||
[94mVect[0m ([95mn[0m [92m+[0m [95mn[0m) [95ma[0m (Type of vapp [95mxs[0m [95mxs[0m)
|
||||
Vect (n + n) a (Type of vapp xs xs)
|
||||
with
|
||||
[94mVect[0m ([92mplus[0m [95mn[0m [95mm[0m) [95ma[0m (Expected type)
|
||||
Vect (plus n m) a (Expected type)
|
||||
|
||||
Specifically:
|
||||
Can't unify
|
||||
[92mplus[0m [95mn[0m [95mn[0m
|
||||
plus n n
|
||||
with
|
||||
[92mplus[0m [95mn[0m [95mm[0m
|
||||
plus n m
|
||||
tutorial006b.idr:10:10:
|
||||
When elaborating right hand side of with block in Main.parity:
|
||||
Can't unify
|
||||
[94mParity[0m ([92mplus[0m ([91mS[0m [95mj[0m) ([91mS[0m [95mj[0m)) (Type of [91meven[0m)
|
||||
Parity (plus (S j) (S j)) (Type of even)
|
||||
with
|
||||
[94mParity[0m ([91mS[0m ([91mS[0m ([92mplus[0m [95mj[0m [95mj[0m))) (Expected type)
|
||||
Parity (S (S (plus j j))) (Expected type)
|
||||
|
||||
Specifically:
|
||||
Can't unify
|
||||
[92mplus[0m ([91mS[0m [95mj[0m) ([91mS[0m [95mj[0m)
|
||||
plus (S j) (S j)
|
||||
with
|
||||
[91mS[0m ([91mS[0m ([92mplus[0m [95mj[0m [95mj[0m))
|
||||
S (S (plus j j))
|
||||
|
@ -1,4 +1,4 @@
|
||||
#!/usr/bin/env bash
|
||||
idris --consolewidth 80 $@ tutorial006a.idr --check
|
||||
idris --consolewidth 80 $@ tutorial006b.idr --check
|
||||
idris --nocolour --consolewidth 80 $@ tutorial006a.idr --check
|
||||
idris --nocolour --consolewidth 80 $@ tutorial006b.idr --check
|
||||
rm -f *.ibc
|
||||
|
@ -3,17 +3,17 @@
|
||||
38,36,34,32,30,28,26,24,22,20,18,16,14,12,10,8,6,4,2,0,END
|
||||
38,36,34,32,30,28,26,24,22,20,18,16,14,12,10,8,6,4,2,0,END
|
||||
unique001a.idr:33:11:Can't convert
|
||||
[94mInt[0m -> [94mString[0m
|
||||
Int -> String
|
||||
with
|
||||
UniqueType ([94mInt[0m -> [94mString[0m)
|
||||
UniqueType (Int -> String)
|
||||
unique001a.idr:44:12:Can't convert
|
||||
[94mInt[0m -> [94mString[0m
|
||||
Int -> String
|
||||
with
|
||||
UniqueType ([94mInt[0m -> [94mString[0m)
|
||||
UniqueType (Int -> String)
|
||||
unique001a.idr:55:12:Can't convert
|
||||
UniqueType ([94mInt[0m -> [94mString[0m)
|
||||
UniqueType (Int -> String)
|
||||
with
|
||||
[94mInt[0m -> [94mString[0m
|
||||
Int -> String
|
||||
unique001b.idr:16:7:Borrowed name xs must not be used on RHS
|
||||
unique001c.idr:46:6:Unique name f is used more than once
|
||||
unique001d.idr:3:7:Borrowed name x must not be used on RHS
|
||||
|
@ -1,9 +1,9 @@
|
||||
#!/usr/bin/env bash
|
||||
idris --consolewidth 80 $@ unique001.idr -o unique001
|
||||
idris --nocolour --consolewidth 80 $@ unique001.idr -o unique001
|
||||
./unique001
|
||||
idris --consolewidth 80 $@ unique001a.idr --check
|
||||
idris --consolewidth 80 $@ unique001b.idr --check
|
||||
idris --consolewidth 80 $@ unique001c.idr --check
|
||||
idris --consolewidth 80 $@ unique001d.idr --check
|
||||
idris --consolewidth 80 $@ unique001e.idr --check
|
||||
idris --nocolour --consolewidth 80 $@ unique001a.idr --check
|
||||
idris --nocolour --consolewidth 80 $@ unique001b.idr --check
|
||||
idris --nocolour --consolewidth 80 $@ unique001c.idr --check
|
||||
idris --nocolour --consolewidth 80 $@ unique001d.idr --check
|
||||
idris --nocolour --consolewidth 80 $@ unique001e.idr --check
|
||||
rm -f unique001 *.ibc
|
||||
|
@ -1,5 +1,5 @@
|
||||
unique002.idr:15:5:Unique name xs is used more than once
|
||||
unique002a.idr:15:5:Can't convert
|
||||
[94mInt[0m -> [94mString[0m
|
||||
Int -> String
|
||||
with
|
||||
UniqueType ([94mInt[0m -> [94mString[0m)
|
||||
UniqueType (Int -> String)
|
||||
|
@ -1,4 +1,4 @@
|
||||
#!/usr/bin/env bash
|
||||
idris --consolewidth 80 $@ unique002.idr --check
|
||||
idris --consolewidth 80 $@ unique002a.idr --check
|
||||
idris --nocolour --consolewidth 80 $@ unique002.idr --check
|
||||
idris --nocolour --consolewidth 80 $@ unique002a.idr --check
|
||||
rm -f *.ibc
|
||||
|
@ -1,4 +1,4 @@
|
||||
unique003.idr:18:5:Can't convert
|
||||
[94mInt[0m -> [94mString[0m
|
||||
Int -> String
|
||||
with
|
||||
UniqueType ([94mInt[0m -> [94mString[0m)
|
||||
UniqueType (Int -> String)
|
||||
|
@ -1,3 +1,3 @@
|
||||
#!/usr/bin/env bash
|
||||
idris --consolewidth 80 $@ unique003.idr --check
|
||||
idris --nocolour --consolewidth 80 $@ unique003.idr --check
|
||||
rm -f *.ibc
|
||||
|
Loading…
Reference in New Issue
Block a user