mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-09-21 05:57:38 +03:00
Add blank line after "large" messages
This commit is contained in:
parent
6e98ac176f
commit
79351ee7ae
@ -98,7 +98,7 @@ iWarn fc err =
|
||||
layoutSource _ _ = Nothing
|
||||
|
||||
layoutWarning :: OutputDoc -> Maybe OutputDoc -> OutputDoc -> OutputDoc
|
||||
layoutWarning loc (Just src) err = loc <$$> src <$$> err
|
||||
layoutWarning loc (Just src) err = loc <$$> src <$$> err <$$> empty
|
||||
layoutWarning loc Nothing err = loc </> err
|
||||
|
||||
|
||||
|
@ -3,9 +3,11 @@ test006.idr:25:23-27:
|
||||
25 | Main.parity_lemma_2 = proof {
|
||||
| ~~~~~
|
||||
This style of tactic proof is deprecated. See %runElab for the replacement.
|
||||
|
||||
test006.idr:32:23-27:
|
||||
|
|
||||
32 | Main.parity_lemma_1 = proof {
|
||||
| ~~~~~
|
||||
This style of tactic proof is deprecated. See %runElab for the replacement.
|
||||
|
||||
[False, True, False, True, False, True]
|
||||
|
@ -10,5 +10,6 @@ When checking an application of function Prelude.List.reverse:
|
||||
Vect n a (Type of xs)
|
||||
and
|
||||
List a (Expected type)
|
||||
|
||||
[3, 2, 1]
|
||||
"Number 42"
|
||||
|
@ -5,6 +5,7 @@ Faulty.idr:6:9-11:
|
||||
| ~~~
|
||||
num is bound as an implicit
|
||||
Did you mean to refer to A.num?
|
||||
|
||||
Faulty.idr:7:7-12:
|
||||
|
|
||||
7 | fault = Refl
|
||||
@ -22,8 +23,10 @@ Specifically:
|
||||
0
|
||||
and
|
||||
num
|
||||
|
||||
Multiple.idr:3:21:
|
||||
|
|
||||
3 | import Data.Vect as X
|
||||
| ^
|
||||
import alias not unique: "X"
|
||||
|
||||
|
@ -5,3 +5,4 @@ basic017a.idr:11:8:
|
||||
When checking type of Main.append:
|
||||
When checking an application of Main.Vect:
|
||||
No such variable n
|
||||
|
||||
|
@ -4,12 +4,14 @@ basic018.idr:7:12-16:
|
||||
| ~~~~~
|
||||
thing is bound as an implicit
|
||||
Did you mean to refer to Main.thing?
|
||||
|
||||
basic018.idr:12:8-12:
|
||||
|
|
||||
12 | test : thing = S 41
|
||||
| ~~~~~
|
||||
thing is bound as an implicit
|
||||
Did you mean to refer to Main.thing?
|
||||
|
||||
basic018.idr:13:6-11:
|
||||
|
|
||||
13 | test = Refl
|
||||
@ -27,3 +29,4 @@ Specifically:
|
||||
42
|
||||
and
|
||||
thing
|
||||
|
||||
|
@ -4,33 +4,39 @@ directives001.idr:14:7:
|
||||
| ^
|
||||
Use of deprecated name directives001.Foo
|
||||
To be replaced with `Bar`.
|
||||
|
||||
directives001.idr:14:7:
|
||||
|
|
||||
14 | mkFoo : String -> Foo
|
||||
| ^
|
||||
Use of deprecated name directives001.Foo
|
||||
To be replaced with `Bar`.
|
||||
|
||||
directives001.idr:15:7-13:
|
||||
|
|
||||
15 | mkFoo = MkFoo
|
||||
| ~~~~~~~
|
||||
Use of deprecated name directives001.Foo
|
||||
To be replaced with `Bar`.
|
||||
|
||||
directives001.idr:15:7-13:
|
||||
|
|
||||
15 | mkFoo = MkFoo
|
||||
| ~~~~~~~
|
||||
Use of deprecated name directives001.Foo
|
||||
To be replaced with `Bar`.
|
||||
|
||||
directives001.idr:26:8-28:28:
|
||||
|
|
||||
26 | main = do
|
||||
| ~~~~ ...
|
||||
Use of a fragile construct directives001.mkBar
|
||||
How `Bar`s are to be created is still being discussed, `mkBar` is subject to change.
|
||||
|
||||
directives001.idr:26:8-28:28:
|
||||
|
|
||||
26 | main = do
|
||||
| ~~~~ ...
|
||||
Use of a fragile construct directives001.mkBar
|
||||
How `Bar`s are to be created is still being discussed, `mkBar` is subject to change.
|
||||
|
||||
|
@ -3,3 +3,4 @@ directives002.idr:12:3-14:28:
|
||||
12 | main = do
|
||||
| ~~~~~~~~~ ...
|
||||
directives002.Main.main is possibly not total due to: directives002.loop
|
||||
|
||||
|
@ -3,6 +3,7 @@ hangman.idr:204:8-12:
|
||||
204 | wlen = proof search
|
||||
| ~~~~~
|
||||
This style of tactic proof is deprecated. See %runElab for the replacement.
|
||||
|
||||
------------
|
||||
|
||||
6 guesses left
|
||||
|
@ -10,3 +10,4 @@ Universe inconsistency.
|
||||
ConstraintFC {uconstraint = ./test002.idr.z <= ./test002.idr.a1, ufc = test002.idr:1:6}
|
||||
ConstraintFC {uconstraint = ./test002.idr.y < ./test002.idr.z, ufc = test002.idr:1:6}
|
||||
ConstraintFC {uconstraint = ./test002.idr.z <= ./test002.idr.a1, ufc = test002.idr:1:6}
|
||||
|
||||
|
@ -6,3 +6,4 @@ When checking right hand side of bad with expected type
|
||||
Tm [] TUnit
|
||||
|
||||
DSL type error: (t(504) => t'(503)) doesn't match ()
|
||||
|
||||
|
@ -7,6 +7,7 @@ When checking right hand side of badCadr1 with expected type
|
||||
|
||||
When checking argument cons2 to function FunErrTest.cadr:
|
||||
Could not prove that [] has at least two elements.
|
||||
|
||||
FunErrTest.idr:38:12-19:
|
||||
|
|
||||
38 | badCadr2 = cadr [1]
|
||||
@ -16,3 +17,4 @@ When checking right hand side of badCadr2 with expected type
|
||||
|
||||
When checking argument cons2 to function FunErrTest.cadr:
|
||||
Could not prove that [] has at least two elements.
|
||||
|
||||
|
@ -8,6 +8,7 @@ When checking right hand side of two with expected type
|
||||
When checking argument prf to function Data.Fin.fromInteger:
|
||||
When using 2 as a literal for a Fin 2
|
||||
2 is not strictly less than 2
|
||||
|
||||
error005.idr:14:12:
|
||||
|
|
||||
14 | hahaha n = 0
|
||||
@ -18,6 +19,7 @@ When checking right hand side of hahaha with expected type
|
||||
When checking argument prf to function Data.Fin.fromInteger:
|
||||
When using 0 as a literal for a Fin n
|
||||
0 is not strictly less than n
|
||||
|
||||
error005.idr:20:11:
|
||||
|
|
||||
20 | notOk n = 2
|
||||
@ -28,6 +30,7 @@ When checking right hand side of notOk with expected type
|
||||
When checking argument prf to function Data.Fin.fromInteger:
|
||||
When using 2 as a literal for a Fin (S (S n))
|
||||
2 is not strictly less than S (S n)
|
||||
|
||||
error005.idr:23:12-24:
|
||||
|
|
||||
23 | b0rken n = fromInteger n
|
||||
@ -39,6 +42,7 @@ When checking argument prf to function Data.Fin.fromInteger:
|
||||
When using n as a literal for a Fin 3
|
||||
Could not show that n is less than 3 because n is a bound
|
||||
variable instead of a constant Integer
|
||||
|
||||
error005.idr:26:17:
|
||||
|
|
||||
26 | x = the (Fin 4) 5
|
||||
@ -49,3 +53,4 @@ When checking right hand side of x with expected type
|
||||
When checking argument prf to function Data.Fin.fromInteger:
|
||||
When using 5 as a literal for a Fin 4
|
||||
5 is not strictly less than 4
|
||||
|
||||
|
@ -4,3 +4,4 @@ WithPatsNoWith.idr:4:1-13:
|
||||
| ~~~~~~~~~~~~~
|
||||
When checking left hand side of foo:
|
||||
unexpected patterns outside of "with" block
|
||||
|
||||
|
@ -16,3 +16,4 @@ When checking argument code to function Main.send_page:
|
||||
Bits32
|
||||
and
|
||||
Int
|
||||
|
||||
|
@ -4,9 +4,11 @@ error008.idr:3:4:
|
||||
| ^
|
||||
When checking type of Main.s2:
|
||||
Can't disambiguate name: Prelude.List.Nil, Data.Vect.Nil
|
||||
|
||||
error008a.idr:3:4:
|
||||
|
|
||||
3 | s1 : Num a => {x : a} -> x + sum {a} Nil = x -- * fromInteger 0
|
||||
| ^
|
||||
When checking type of Main.s1:
|
||||
Can't disambiguate name: Prelude.List.Nil, Data.Vect.Nil
|
||||
|
||||
|
@ -3,3 +3,4 @@ test023.idr:20:26-36:
|
||||
20 | %provide (t : Type) with badProvider
|
||||
| ~~~~~~~~~~~
|
||||
Type provider error: Always fails
|
||||
|
||||
|
@ -3,3 +3,4 @@ interfaces008.idr:20:18-23:
|
||||
20 | implementation Foo2 a where
|
||||
| ~~~~~~
|
||||
Default implementations must be for a super interface constraint on the containing interface.
|
||||
|
||||
|
@ -67,6 +67,7 @@ When checking right hand side of term with expected type
|
||||
|
||||
When checking an application of function Prelude.Applicative.pure:
|
||||
No such variable f
|
||||
|
||||
./mplus2.idr:17:37:
|
||||
|
|
||||
17 | `mplus` pure f
|
||||
|
@ -3,6 +3,7 @@
|
||||
1 | Broken
|
||||
| ^
|
||||
Program line next to comment
|
||||
|
||||
'a'
|
||||
'd'
|
||||
zabcdefg
|
||||
|
@ -4,6 +4,7 @@ DataDef.idr:74:1-8:
|
||||
| ~~~~~~~~
|
||||
While running an elaboration script, the following error occurred:
|
||||
Prelude.Either.Either is already defined as a datatype.
|
||||
|
||||
Tacs.idr:299:15-300:78:
|
||||
|
|
||||
299 | testElab3 = %runElab (elaborateSTLC (App (Lam "x" (App (Var 0) (Var 0)))
|
||||
@ -12,6 +13,7 @@ When checking right hand side of testElab3 with expected type
|
||||
DPair Ty (Tm [])
|
||||
|
||||
Unifying ty and ARR ty t would lead to infinite value
|
||||
|
||||
AgdaStyleReflection.idr:315:5-20:
|
||||
|
|
||||
315 | baz = tactic trivial
|
||||
@ -20,3 +22,4 @@ When checking right hand side of baz with expected type
|
||||
(Nat, Void)
|
||||
|
||||
PROOF SEARCH FAILURE is not defined.
|
||||
|
||||
|
@ -7,3 +7,4 @@ Type mismatch between
|
||||
()
|
||||
and
|
||||
String
|
||||
|
||||
|
@ -4,3 +4,4 @@ meta004.idr:50:1-8:
|
||||
| ~~~~~~~~
|
||||
While running an elaboration script, the following error occurred:
|
||||
Not an impossible case
|
||||
|
||||
|
@ -3,8 +3,10 @@ test029.idr:29:25-29:
|
||||
29 | simple.append_lemma_2 = proof {
|
||||
| ~~~~~
|
||||
This style of tactic proof is deprecated. See %runElab for the replacement.
|
||||
|
||||
test029.idr:36:25-29:
|
||||
|
|
||||
36 | simple.append_lemma_1 = proof {
|
||||
| ~~~~~
|
||||
This style of tactic proof is deprecated. See %runElab for the replacement.
|
||||
|
||||
|
@ -3,16 +3,19 @@ Reflect.idr:175:21-25:
|
||||
175 | Reflect.appRExpr1 = proof {
|
||||
| ~~~~~
|
||||
This style of tactic proof is deprecated. See %runElab for the replacement.
|
||||
|
||||
Reflect.idr:184:21-25:
|
||||
|
|
||||
184 | Reflect.appRExpr2 = proof {
|
||||
| ~~~~~
|
||||
This style of tactic proof is deprecated. See %runElab for the replacement.
|
||||
|
||||
Reflect.idr:192:15-19:
|
||||
|
|
||||
192 | Reflect.bp1 = proof {
|
||||
| ~~~~~
|
||||
This style of tactic proof is deprecated. See %runElab for the replacement.
|
||||
|
||||
test030a.idr:12:26-37:
|
||||
|
|
||||
12 | testReflect1 {a} xs ys = AssocProof a
|
||||
@ -31,3 +34,4 @@ When checking an application of function Reflect.getJust:
|
||||
Just x
|
||||
and
|
||||
Nothing
|
||||
|
||||
|
@ -3,31 +3,37 @@ Parity.idr:17:18-22:
|
||||
17 | parity_lemma_2 = proof {
|
||||
| ~~~~~
|
||||
This style of tactic proof is deprecated. See %runElab for the replacement.
|
||||
|
||||
Parity.idr:24:18-22:
|
||||
|
|
||||
24 | parity_lemma_1 = proof {
|
||||
| ~~~~~
|
||||
This style of tactic proof is deprecated. See %runElab for the replacement.
|
||||
|
||||
test015.idr:88:15-19:
|
||||
|
|
||||
88 | Main.ntbOdd = proof {
|
||||
| ~~~~~
|
||||
This style of tactic proof is deprecated. See %runElab for the replacement.
|
||||
|
||||
test015.idr:97:16-20:
|
||||
|
|
||||
97 | Main.ntbEven = proof {
|
||||
| ~~~~~
|
||||
This style of tactic proof is deprecated. See %runElab for the replacement.
|
||||
|
||||
test015.idr:107:20-24:
|
||||
|
|
||||
107 | Main.adc_lemma_2 = proof {
|
||||
| ~~~~~
|
||||
This style of tactic proof is deprecated. See %runElab for the replacement.
|
||||
|
||||
test015.idr:142:20-24:
|
||||
|
|
||||
142 | Main.adc_lemma_1 = proof {
|
||||
| ~~~~~
|
||||
This style of tactic proof is deprecated. See %runElab for the replacement.
|
||||
|
||||
00101010
|
||||
01011001
|
||||
010000011
|
||||
|
@ -7,3 +7,4 @@ When checking right hand side of test with expected type
|
||||
|
||||
When checking argument arg to function DefaultArgUnknownName.funWithBadDefArg:
|
||||
No such variable sadgjhsag
|
||||
|
||||
|
@ -3,3 +3,4 @@ ClaimAndUnfocus.idr:8:27-31:
|
||||
8 | ClaimAndUnfocus.foo_rhs = proof
|
||||
| ~~~~~
|
||||
This style of tactic proof is deprecated. See %runElab for the replacement.
|
||||
|
||||
|
@ -11,6 +11,7 @@ rewriting xs ++ ys ++ xs to (xs ++ ys) ++ xs did not change type x ::
|
||||
x ::
|
||||
(xs ++ ys) ++
|
||||
zs
|
||||
|
||||
proof011a.idr:14:5-37:
|
||||
|
|
||||
14 | = rewrite vassoc xs ys xs in Refl
|
||||
@ -24,3 +25,4 @@ rewriting xs ++ ys ++ xs to (xs ++ ys) ++ xs did not change type x ::
|
||||
x ::
|
||||
(xs ++ ys) ++
|
||||
zs
|
||||
|
||||
|
@ -6,3 +6,4 @@ When checking right hand side of zzz with expected type
|
||||
TT
|
||||
|
||||
No such variable k
|
||||
|
||||
|
@ -3,16 +3,19 @@ Quasiquote004.idr:39:26-30:
|
||||
39 | Quasiquote004.getMeNat = proof
|
||||
| ~~~~~
|
||||
This style of tactic proof is deprecated. See %runElab for the replacement.
|
||||
|
||||
Quasiquote004.idr:42:28-32:
|
||||
|
|
||||
42 | Quasiquote004.fizzyIsAOK = proof
|
||||
| ~~~~~
|
||||
This style of tactic proof is deprecated. See %runElab for the replacement.
|
||||
|
||||
Quasiquote004.idr:50:27-31:
|
||||
|
|
||||
50 | Quasiquote004.getMeNat' = proof
|
||||
| ~~~~~
|
||||
This style of tactic proof is deprecated. See %runElab for the replacement.
|
||||
|
||||
Quasiquote004.idr:50:25-51:18:
|
||||
|
|
||||
50 | Quasiquote004.getMeNat' = proof
|
||||
@ -21,3 +24,4 @@ When checking right hand side of Quasiquote004.getMeNat' with expected type
|
||||
String
|
||||
|
||||
Not a Nat goal
|
||||
|
||||
|
@ -7,6 +7,7 @@ When checking right hand side of b with expected type
|
||||
|
||||
Can't disambiguate name: ForeignEnv.Nil,
|
||||
Prelude.List.Nil
|
||||
|
||||
quasiquote006.idr:12:3-17:
|
||||
|
|
||||
12 | c = `{alsdkjflkj}
|
||||
@ -15,6 +16,7 @@ When checking right hand side of c with expected type
|
||||
TTName
|
||||
|
||||
No such variable alsdkjflkj
|
||||
|
||||
quasiquote006.idr:15:3-11:
|
||||
|
|
||||
15 | d = `{(::)}
|
||||
@ -25,4 +27,5 @@ When checking right hand side of d with expected type
|
||||
Can't disambiguate name: ForeignEnv.::,
|
||||
Prelude.List.::,
|
||||
Prelude.Stream.::
|
||||
|
||||
quasiquote006.idr:17:3:Main.d already defined
|
||||
|
@ -3,9 +3,11 @@ reg017.idr:5:17-23:
|
||||
5 | { default tactics { refine Refl; solve; } prfA : a = a } ->
|
||||
| ~~~~~~~
|
||||
This style of tactic proof is deprecated. See %runElab for the replacement.
|
||||
|
||||
reg017.idr:8:17-23:
|
||||
|
|
||||
8 | { default tactics { refine Refl; solve; } prfBC : b = c } ->
|
||||
| ~~~~~~~
|
||||
This style of tactic proof is deprecated. See %runElab for the replacement.
|
||||
|
||||
4
|
||||
|
@ -4,3 +4,4 @@ reg027a.idr:9:16-30:
|
||||
9 | implementation Show (Int -> b) where
|
||||
| ~~~~~~~~~~~~~~~
|
||||
Overlapping implementation: Show (Int -> a) already defined
|
||||
|
||||
|
@ -4,28 +4,33 @@ reg003a.idr:4:13-38:
|
||||
| ~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
When checking type of Main.ECons:
|
||||
No such variable OddList
|
||||
|
||||
reg003a.idr:7:13-38:
|
||||
|
|
||||
7 | OCons : Nat -> EvenList -> OddList
|
||||
| ~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
When checking type of Main.OCons:
|
||||
No such variable EvenList
|
||||
|
||||
reg003a.idr:9:6:
|
||||
|
|
||||
9 | test : EvenList
|
||||
| ^
|
||||
When checking type of Main.test:
|
||||
No such variable EvenList
|
||||
|
||||
reg006.idr:17:1-23:
|
||||
|
|
||||
17 | lookup k Leaf = Nothing
|
||||
| ~~~~~~~~~~~~~~~~~~~~~~~
|
||||
RBTree.lookup is possibly not total due to recursive path RBTree.lookup --> RBTree.lookup
|
||||
|
||||
reg007.lidr:8:3-13:
|
||||
|
|
||||
8 | > A.n = Z -- This is where it's at!
|
||||
| ~~~~~~~~~~~
|
||||
A.n is already defined
|
||||
|
||||
reg007.lidr:12:13-18:
|
||||
|
|
||||
12 | > hurrah = isSame
|
||||
@ -43,42 +48,50 @@ Specifically:
|
||||
1
|
||||
and
|
||||
0
|
||||
|
||||
reg010.idr:5:3-26:
|
||||
|
|
||||
5 | unsafeSubst P x x px | _ = px
|
||||
| ~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
When checking left hand side of with block in usubst.unsafeSubst:
|
||||
Can't match on with block in usubst.unsafeSubst warg a P x x px
|
||||
|
||||
reg018a.idr:16:1-18:
|
||||
|
|
||||
16 | minusCoNat Z n = Z
|
||||
| ~~~~~~~~~~~~~~~~~~
|
||||
conat.minusCoNat is possibly not total due to recursive path conat.minusCoNat --> conat.minusCoNat
|
||||
|
||||
reg018a.idr:21:1-42:
|
||||
|
|
||||
21 | loopForever = minusCoNat infinity infinity
|
||||
| ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
conat.loopForever is possibly not total due to: conat.minusCoNat
|
||||
|
||||
reg018b.idr:8:1-28:
|
||||
|
|
||||
8 | showB (I x) = "I" ++ showB x
|
||||
| ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
A.showB is possibly not total due to recursive path A.showB --> A.showB
|
||||
|
||||
reg018b.idr:11:1-6:
|
||||
|
|
||||
11 | Show B where show = showB
|
||||
| ~~~~~~
|
||||
A.B implementation of Prelude.Show.Show is possibly not total due to: A.showB
|
||||
|
||||
reg018c.idr:21:1-22:21:
|
||||
|
|
||||
21 | inf (x :: xs) with (hdtl xs)
|
||||
| ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...
|
||||
CodataTest.inf is possibly not total due to: with block in CodataTest.inf
|
||||
|
||||
reg018d.idr:8:1-39:
|
||||
|
|
||||
8 | pull {n=Z} _ (x :: xs) = (x, xs)
|
||||
| ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
Main.pull is not total as there are missing cases
|
||||
|
||||
reg023.idr:7:5-7:
|
||||
|
|
||||
7 | bad = Z
|
||||
@ -90,43 +103,51 @@ Type mismatch between
|
||||
Nat (Type of 0)
|
||||
and
|
||||
f Nat (Expected type)
|
||||
|
||||
reg028.idr:5:1-9:
|
||||
|
|
||||
5 | bad Z = Z
|
||||
| ~~~~~~~~~
|
||||
tbad.bad is possibly not total due to: with block in tbad.bad
|
||||
|
||||
reg028a.idr:17:14-18:
|
||||
|
|
||||
17 | qsortLemma = proof
|
||||
| ~~~~~
|
||||
This style of tactic proof is deprecated. See %runElab for the replacement.
|
||||
|
||||
reg028a.idr:11:1-14:
|
||||
|
|
||||
11 | qsort' [] = []
|
||||
| ~~~~~~~~~~~~~~
|
||||
tbad.qsort' is possibly not total due to: with block in tbad.qsort'
|
||||
|
||||
reg034.idr:6:1-14:
|
||||
|
|
||||
6 | bar xs xs Refl = Refl
|
||||
| ~~~~~~~~~~~~~~
|
||||
When checking left hand side of bar:
|
||||
Can't match on bar xs xs Refl
|
||||
|
||||
reg034.idr:9:1-14:
|
||||
|
|
||||
9 | foo f x x Refl = Refl
|
||||
| ~~~~~~~~~~~~~~
|
||||
When checking left hand side of foo:
|
||||
Can't match on foo f x x Refl
|
||||
|
||||
reg035b.idr:8:12-38:
|
||||
|
|
||||
8 | fins Z = ([] ** (finZEmpty {a=_}))
|
||||
| ~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
No such variable __pi_arg
|
||||
|
||||
reg044.idr:4:6-10:
|
||||
|
|
||||
4 | pf = proof
|
||||
| ~~~~~
|
||||
This style of tactic proof is deprecated. See %runElab for the replacement.
|
||||
|
||||
reg044.idr:4:4-6:13:
|
||||
|
|
||||
4 | pf = proof
|
||||
@ -144,12 +165,14 @@ Specifically:
|
||||
b
|
||||
and
|
||||
a
|
||||
|
||||
reg049.idr:2:11-14:
|
||||
|
|
||||
2 | Bogus : Void
|
||||
| ~~~~
|
||||
When checking constructor Main.Bogus:
|
||||
Void is not Main.Foo
|
||||
|
||||
reg049.idr:5:6-12:
|
||||
|
|
||||
5 | uhOh = Bogus
|
||||
@ -158,6 +181,7 @@ When checking right hand side of uhOh with expected type
|
||||
Void
|
||||
|
||||
No such variable Bogus
|
||||
|
||||
./badbangop.idr:7:1:
|
||||
|
|
||||
7 | (!) : List a -> Nat -> Maybe a
|
||||
@ -177,18 +201,21 @@ reg054.idr:18:1-17:
|
||||
When checking left hand side of inf:
|
||||
When checking an application of constructor Main.MkInfer:
|
||||
Attempting concrete match on polymorphic argument: 0
|
||||
|
||||
reg054.idr:34:1-18:
|
||||
|
|
||||
34 | weird {x = Char} y = '5'
|
||||
| ~~~~~~~~~~~~~~~~~~
|
||||
When checking left hand side of weird:
|
||||
No explicit types on left hand side: Char
|
||||
|
||||
reg054.idr:37:1-30:
|
||||
|
|
||||
37 | weird' {x = Prelude.Nat.Nat} y = Z
|
||||
| ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
When checking left hand side of weird':
|
||||
No explicit types on left hand side: Nat
|
||||
|
||||
reg054.idr:40:1-7:
|
||||
|
|
||||
40 | tctrick (Just x) = x
|
||||
@ -199,18 +226,21 @@ When checking an application of Main.tctrick:
|
||||
Maybe a1 (Type of Just x)
|
||||
and
|
||||
a (Expected type)
|
||||
|
||||
reg055.idr:5:1-7:
|
||||
|
|
||||
5 | g (f Z) = 1
|
||||
| ~~~~~~~
|
||||
When checking left hand side of g:
|
||||
Can't match on g (f 0)
|
||||
|
||||
reg055.idr:8:1-5:
|
||||
|
|
||||
8 | h x x = x
|
||||
| ~~~~~
|
||||
When checking left hand side of h:
|
||||
Can't match on h x x
|
||||
|
||||
reg055a.idr:8:1-18:
|
||||
|
|
||||
8 | foo (CAny Nothing) = 42
|
||||
@ -218,56 +248,66 @@ reg055a.idr:8:1-18:
|
||||
When checking left hand side of foo:
|
||||
When checking an application of constructor Foo.CAny:
|
||||
Attempting concrete match on polymorphic argument: Nothing
|
||||
|
||||
reg055a.idr:13:1-23:
|
||||
|
|
||||
13 | apply (\x => \y => x) a = a
|
||||
| ~~~~~~~~~~~~~~~~~~~~~~~
|
||||
When checking left hand side of Foo.apply:
|
||||
Can't match on apply (\x, y => x) a
|
||||
|
||||
reg056.idr:7:16-25:
|
||||
|
|
||||
7 | dodgy n m Refl impossible
|
||||
| ~~~~~~~~~~
|
||||
dodgy n m Refl is a valid case
|
||||
|
||||
reg056.idr:10:11-20:
|
||||
|
|
||||
10 | nonk Refl impossible
|
||||
| ~~~~~~~~~~
|
||||
nonk Refl is a valid case
|
||||
|
||||
reg068.idr:1:6-8:
|
||||
|
|
||||
1 | data nat : Type where --error
|
||||
| ~~~
|
||||
Main.nat has a name which may be implicitly bound.
|
||||
This is likely to lead to problems!
|
||||
|
||||
reg068.idr:2:8-10:
|
||||
|
|
||||
2 | ze : nat --hello.idr:10:6:When checking constructor Main.ze: !!V 0!! is not Main.nat
|
||||
| ~~~
|
||||
Main.ze has a name which may be implicitly bound.
|
||||
This is likely to lead to problems!
|
||||
|
||||
reg068.idr:2:8-10:
|
||||
|
|
||||
2 | ze : nat --hello.idr:10:6:When checking constructor Main.ze: !!V 0!! is not Main.nat
|
||||
| ~~~
|
||||
nat is bound as an implicit
|
||||
Did you mean to refer to Main.nat?
|
||||
|
||||
reg068.idr:2:8-10:
|
||||
|
|
||||
2 | ze : nat --hello.idr:10:6:When checking constructor Main.ze: !!V 0!! is not Main.nat
|
||||
| ~~~
|
||||
When checking constructor Main.ze:
|
||||
Type level variable nat is not Main.nat
|
||||
|
||||
Mod.idr:11:1-22:
|
||||
|
|
||||
11 | natexp k = S (natfn k)
|
||||
| ~~~~~~~~~~~~~~~~~~~~~~
|
||||
public export Mod.natexp can't refer to export Mod.natfn
|
||||
|
||||
reg070.idr:7:1-7:
|
||||
|
|
||||
7 | Show Te where
|
||||
| ~~~~~~~
|
||||
Test_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
|
||||
|
||||
./reg076.idr:8:1:
|
||||
|
|
||||
8 | <empty line>
|
||||
@ -298,13 +338,16 @@ When checking argument value to function Prelude.Basics.the:
|
||||
-0.0
|
||||
and
|
||||
0.0
|
||||
|
||||
Canonicity.idr:9:1-9:
|
||||
|
|
||||
9 | f Nil = 0
|
||||
| ~~~~~~~~~
|
||||
Canonicity.f is not total as there are missing cases
|
||||
|
||||
Canonicity.idr:12:1-20:
|
||||
|
|
||||
12 | NaN = f (Cons 0 Nil)
|
||||
| ~~~~~~~~~~~~~~~~~~~~
|
||||
Canonicity.NaN is possibly not total due to: Canonicity.f
|
||||
|
||||
|
@ -3,21 +3,25 @@ SourceLoc.idr:12:19-25:
|
||||
12 | getLoc : {default tactics { sourceLocation } x : SourceLocation} -> SourceLocation
|
||||
| ~~~~~~~
|
||||
This style of tactic proof is deprecated. See %runElab for the replacement.
|
||||
|
||||
SourceLoc.idr:21:19-23:
|
||||
|
|
||||
21 | fromProofScript = proof sourceLocation
|
||||
| ~~~~~
|
||||
This style of tactic proof is deprecated. See %runElab for the replacement.
|
||||
|
||||
SourceLoc.idr:41:20-26:
|
||||
|
|
||||
41 | Die : {default tactics { sourceLocation } loc : SourceLocation} -> Tm ctxt t
|
||||
| ~~~~~~~
|
||||
This style of tactic proof is deprecated. See %runElab for the replacement.
|
||||
|
||||
SourceLoc.idr:99:18-22:
|
||||
|
|
||||
99 | SourceLoc.meta = proof
|
||||
| ~~~~~
|
||||
This style of tactic proof is deprecated. See %runElab for the replacement.
|
||||
|
||||
Testing using definition
|
||||
FileLoc "SourceLoc.idr" (17, 11) (17, 16)
|
||||
Testing using inline tactics
|
||||
|
@ -10,6 +10,7 @@ When checking an application of function Prelude.Interfaces.+:
|
||||
String (Type of "argh")
|
||||
and
|
||||
Nat (Expected type)
|
||||
|
||||
SyntaxTest.idr:5:7-18:
|
||||
|
|
||||
5 | foo = fnord "argh"
|
||||
@ -22,3 +23,4 @@ When checking an application of function Prelude.Interfaces.+:
|
||||
String (Type of "argh")
|
||||
and
|
||||
Nat (Expected type)
|
||||
|
||||
|
@ -3,13 +3,16 @@ test010.idr:15:1-30:
|
||||
15 | foo (MkBad f i) = f (MkBad' i)
|
||||
| ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
Main.foo is possibly not total due to: Main.MkBad
|
||||
|
||||
test010a.idr:9:1-23:
|
||||
|
|
||||
9 | bar = MkBad (\x => 3) 3
|
||||
| ~~~~~~~~~~~~~~~~~~~~~~~
|
||||
main.bar is possibly not total due to: main.MkBad
|
||||
|
||||
test010b.idr:9:1-23:
|
||||
|
|
||||
9 | bar = MkBad (\x => 3) 3
|
||||
| ~~~~~~~~~~~~~~~~~~~~~~~
|
||||
main.bar is possibly not total due to: main.MkBad
|
||||
|
||||
|
@ -3,13 +3,16 @@ test017.idr:94:26-30:
|
||||
94 | maxCommutativeStepCase = proof {
|
||||
| ~~~~~
|
||||
This style of tactic proof is deprecated. See %runElab for the replacement.
|
||||
|
||||
test017a.idr:7:1-24:
|
||||
|
|
||||
7 | vtrans [] _ = []
|
||||
| ~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
scg.vtrans is possibly not total due to recursive path scg.vtrans --> scg.vtrans
|
||||
|
||||
test017b.idr:4:1-9:
|
||||
|
|
||||
4 | foo = foo
|
||||
| ~~~~~~~~~
|
||||
foo.foo is possibly not total due to recursive path foo.foo
|
||||
|
||||
|
@ -3,3 +3,4 @@ totality003a.idr:5:1-13:
|
||||
5 | qsort [] = []
|
||||
| ~~~~~~~~~~~~~
|
||||
smaller.qsort is possibly not total due to recursive path smaller.qsort --> smaller.qsort --> smaller.qsort
|
||||
|
||||
|
@ -4,8 +4,10 @@ totality004a.idr:13:1-44:
|
||||
13 | process (Get f) (x :: xs) = process (f x) xs
|
||||
| ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
Main.process is possibly not total due to recursive path Main.process --> Main.process --> Main.process
|
||||
|
||||
totality004a.idr:24:1-60:
|
||||
|
|
||||
24 | main = printLn (take 10 (process doubleInt (countStream 1)))
|
||||
| ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
Main.main is possibly not total due to: Main.process
|
||||
|
||||
|
@ -3,13 +3,16 @@ totality006.idr:8:1-29:
|
||||
8 | prf Z Z Oh impossible
|
||||
| ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
Main.prf is not total as there are missing cases
|
||||
|
||||
totality006a.idr:11:21-30:
|
||||
|
|
||||
11 | prf' (S _) (S _) Oh impossible
|
||||
| ~~~~~~~~~~
|
||||
prf' (S _) (S _) Oh is a valid case
|
||||
|
||||
totality006b.idr:10:1-34:
|
||||
|
|
||||
10 | blargh [] (y :: xs) so = absurd so
|
||||
| ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
totality006b.blargh is not total as there are missing cases
|
||||
|
||||
|
@ -4,5 +4,6 @@ Totality.idr:4:1-9:
|
||||
4 | foo Z = Z
|
||||
| ~~~~~~~~~
|
||||
Totality.foo is not total as there are missing cases
|
||||
|
||||
Totality.idr:4:1-9:Could not build: Totality.foo is not total as there are missing cases
|
||||
Leaving directory `./src'
|
||||
|
@ -3,3 +3,4 @@ totality008.idr:7:1-14:
|
||||
7 | ElimT _ C1 = 3
|
||||
| ~~~~~~~~~~~~~~
|
||||
Main.ElimT is possibly not total due to: Main.C2
|
||||
|
||||
|
@ -3,48 +3,58 @@ TestLambdaPossible.idr:9:25-34:
|
||||
9 | wrongPossible = (\Flase impossible)
|
||||
| ~~~~~~~~~~
|
||||
Warning - TestLambdaPossible.case block in wrongPossible at TestLambdaPossible.idr:9:25-34 is not total as there are missing cases
|
||||
|
||||
TestLambdaPossible.idr:9:1-35:
|
||||
|
|
||||
9 | wrongPossible = (\Flase impossible)
|
||||
| ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
Warning - TestLambdaPossible.wrongPossible is possibly not total due to: TestLambdaPossible.case block in wrongPossible at TestLambdaPossible.idr:9:25-34
|
||||
|
||||
TestLambdaPossible.idr:12:25:
|
||||
|
|
||||
12 | wrongPossible' x = case x of
|
||||
| ^
|
||||
Warning - TestLambdaPossible.case block in wrongPossible' at TestLambdaPossible.idr:12:25 is not total as there are missing cases
|
||||
|
||||
TestLambdaPossible.idr:12:1-13:40:
|
||||
|
|
||||
12 | wrongPossible' x = case x of
|
||||
| ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...
|
||||
Warning - TestLambdaPossible.wrongPossible' is possibly not total due to: TestLambdaPossible.case block in wrongPossible' at TestLambdaPossible.idr:12:25
|
||||
|
||||
TestLambdaPossible.idr:9:15-35:
|
||||
|
|
||||
9 | wrongPossible = (\Flase impossible)
|
||||
| ~~~~~~~~~~~~~~~~~~~~~
|
||||
Warning - TestLambdaPossible.case block in wrongPossible at TestLambdaPossible.idr:9:25-34 is not total as there are missing cases
|
||||
|
||||
TestLambdaPossible.idr:9:1-35:
|
||||
|
|
||||
9 | wrongPossible = (\Flase impossible)
|
||||
| ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
Warning - TestLambdaPossible.wrongPossible is possibly not total due to: TestLambdaPossible.case block in wrongPossible at TestLambdaPossible.idr:9:25-34
|
||||
|
||||
TestLambdaPossible.idr:12:18-13:40:
|
||||
|
|
||||
12 | wrongPossible' x = case x of
|
||||
| ~~~~~~~~~~~ ...
|
||||
Warning - TestLambdaPossible.case block in wrongPossible' at TestLambdaPossible.idr:12:25 is not total as there are missing cases
|
||||
|
||||
TestLambdaPossible.idr:12:1-13:40:
|
||||
|
|
||||
12 | wrongPossible' x = case x of
|
||||
| ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...
|
||||
Warning - TestLambdaPossible.wrongPossible' is possibly not total due to: TestLambdaPossible.case block in wrongPossible' at TestLambdaPossible.idr:12:25
|
||||
|
||||
TestLambdaPossible2.idr:10:1-35:
|
||||
|
|
||||
10 | wrongPossible = (\Flase impossible)
|
||||
| ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
TestLambdaPossible.wrongPossible is possibly not total due to: TestLambdaPossible.case block in wrongPossible at TestLambdaPossible2.idr:10:25-34
|
||||
|
||||
TestLambdaPossible2.idr:14:1-15:40:
|
||||
|
|
||||
14 | wrongPossible' x = case x of
|
||||
| ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...
|
||||
TestLambdaPossible.wrongPossible' is possibly not total due to: TestLambdaPossible.case block in wrongPossible' at TestLambdaPossible2.idr:14:25
|
||||
|
||||
|
@ -3,8 +3,10 @@ totality010.idr:27:1-35:
|
||||
27 | evenNotS MkEven ZeroEven impossible
|
||||
| ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
Main.evenNotS is not total as there are missing cases
|
||||
|
||||
totality010.idr:30:1-40:
|
||||
|
|
||||
30 | bad = evenNotS ZeroEven $ MkBad ZeroEven
|
||||
| ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
Main.bad is possibly not total due to: Main.evenNotS
|
||||
|
||||
|
@ -3,3 +3,4 @@ totality011.lidr:22:3-57:
|
||||
22 | > weCanOnlyGetOlder {t'' = Z} {t = Z} _ _ _ = LTEZero
|
||||
| ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
Main.weCanOnlyGetOlder is not total as there are missing cases
|
||||
|
||||
|
@ -3,8 +3,10 @@ totality012a.idr:9:1-10:27:
|
||||
9 | echo2 x = if (x == "quit") then PutStr "Bye!\n"
|
||||
| ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...
|
||||
Main.echo2 is possibly not total due to recursive path Main.echo2 --> Main.echo2
|
||||
|
||||
totality012b.idr:11:1-17:33:
|
||||
|
|
||||
11 | echo = do PutStr "$ "
|
||||
| ~~~~~~~~~~~~~~~~~~~~~ ...
|
||||
Main.echo is possibly not total due to recursive path Main.echo
|
||||
|
||||
|
@ -3,8 +3,10 @@ totality013a.idr:5:3-49:
|
||||
5 | foo order x xs y ys _ = mtot order (x :: xs) ys
|
||||
| ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
Main.foo is possibly not total due to recursive path Main.foo --> Main.mtot --> Main.mtot --> Main.mtot
|
||||
|
||||
totality013a.idr:9:3-36:
|
||||
|
|
||||
9 | mtot order [] right = right
|
||||
| ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
Main.mtot is possibly not total due to: Main.foo
|
||||
|
||||
|
@ -10,3 +10,4 @@ Universe inconsistency.
|
||||
ConstraintFC {uconstraint = ./totality014.idr.w < ./totality014.idr.u, ufc = totality014.idr:1:6-9}
|
||||
ConstraintFC {uconstraint = ./totality014.idr.w < ./totality014.idr.u, ufc = totality014.idr:1:6-9}
|
||||
ConstraintFC {uconstraint = ./totality014.idr.u <= ./totality014.idr.w, ufc = totality014.idr:6:27-29}
|
||||
|
||||
|
@ -3,13 +3,16 @@ totality015a.idr:52:3-53:
|
||||
52 | quiz (num1 :: num2 :: nums) score = quiz nums score
|
||||
| ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
Main.quiz is possibly not total due to recursive path Main.quiz --> Main.quiz
|
||||
|
||||
totality015a.idr:42:3-44:36:
|
||||
|
|
||||
42 | correct nums score
|
||||
| ~~~~~~~~~~~~~~~~~~ ...
|
||||
Main.correct is possibly not total due to: Main.quiz
|
||||
|
||||
totality015a.idr:47:3-49:28:
|
||||
|
|
||||
47 | wrong nums ans score
|
||||
| ~~~~~~~~~~~~~~~~~~~~ ...
|
||||
Main.wrong is possibly not total due to: Main.quiz
|
||||
|
||||
|
@ -3,43 +3,52 @@ totality016.idr:15:1-21:
|
||||
15 | f1 (MkTP T1 x) = True
|
||||
| ~~~~~~~~~~~~~~~~~~~~~
|
||||
Main.f1 is not total as there are missing cases
|
||||
|
||||
totality016.idr:19:1-24:
|
||||
|
|
||||
19 | f2 (MkTP T1 x, _) = True
|
||||
| ~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
Main.f2 is not total as there are missing cases
|
||||
|
||||
totality016.idr:23:1-29:
|
||||
|
|
||||
23 | f3 ((MkTP T1 x, _), _) = True
|
||||
| ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
Main.f3 is not total as there are missing cases
|
||||
|
||||
totality016.idr:27:1-14:
|
||||
|
|
||||
27 | g1 T1 x = True
|
||||
| ~~~~~~~~~~~~~~
|
||||
Main.g1 is not total as there are missing cases
|
||||
|
||||
totality016.idr:31:1-17:
|
||||
|
|
||||
31 | g2 (T1, x) = True
|
||||
| ~~~~~~~~~~~~~~~~~
|
||||
Main.g2 is not total as there are missing cases
|
||||
|
||||
totality016.idr:35:1-16:
|
||||
|
|
||||
35 | h1 True x = True
|
||||
| ~~~~~~~~~~~~~~~~
|
||||
Main.h1 is not total as there are missing cases
|
||||
|
||||
totality016.idr:39:1-19:
|
||||
|
|
||||
39 | h2 (True, x) = True
|
||||
| ~~~~~~~~~~~~~~~~~~~
|
||||
Main.h2 is not total as there are missing cases
|
||||
|
||||
totality016.idr:43:1-25:
|
||||
|
|
||||
43 | h3 (MkTP2 (T1, x)) = True
|
||||
| ~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
Main.h3 is not total as there are missing cases
|
||||
|
||||
totality016.idr:47:1-30:
|
||||
|
|
||||
47 | h4 (MkTP2 (T1, x), _) _ = True
|
||||
| ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
Main.h4 is not total as there are missing cases
|
||||
|
||||
|
@ -3,28 +3,34 @@ totality017.idr:19:1-15:
|
||||
19 | g1 T1 T1 = True
|
||||
| ~~~~~~~~~~~~~~~
|
||||
Main.g1 is not total as there are missing cases
|
||||
|
||||
totality017.idr:25:1-17:
|
||||
|
|
||||
25 | g2 T1' T1' = True
|
||||
| ~~~~~~~~~~~~~~~~~
|
||||
Main.g2 is not total as there are missing cases
|
||||
|
||||
totality017.idr:31:1-13:
|
||||
|
|
||||
31 | g3 T1' = True
|
||||
| ~~~~~~~~~~~~~
|
||||
Main.g3 is not total as there are missing cases
|
||||
|
||||
totality017.idr:37:1-36:
|
||||
|
|
||||
37 | g4 (MkTTPP (MkPP 0) (MkPP 0)) = True
|
||||
| ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
Main.g4 is not total as there are missing cases
|
||||
|
||||
totality017.idr:42:1-11:
|
||||
|
|
||||
42 | f' 0 = True
|
||||
| ~~~~~~~~~~~
|
||||
Main.f' is not total as there are missing cases
|
||||
|
||||
totality017.idr:47:1-17:
|
||||
|
|
||||
47 | f (MkPP 0) = True
|
||||
| ~~~~~~~~~~~~~~~~~
|
||||
Main.f is not total as there are missing cases
|
||||
|
||||
|
@ -3,3 +3,4 @@ totality018.idr:12:1-10:
|
||||
12 | bar FZ = 0
|
||||
| ~~~~~~~~~~
|
||||
Main.bar is not total as there are missing cases
|
||||
|
||||
|
@ -3,8 +3,10 @@ totality019.idr:8:1-36:
|
||||
8 | testCov False False = ?testCov_rhs_3
|
||||
| ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
Main.testCov is not total as there are missing cases
|
||||
|
||||
totality019.idr:12:1-42:
|
||||
|
|
||||
12 | testCov' (False ** False) = ?testCov_rhs_3
|
||||
| ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
Main.testCov' is not total as there are missing cases
|
||||
|
||||
|
@ -3,8 +3,10 @@ totality020.idr:4:14-23:
|
||||
4 | bug _ _ Refl impossible
|
||||
| ~~~~~~~~~~
|
||||
bug _ _ Refl is a valid case
|
||||
|
||||
totality020.idr:7:14-23:
|
||||
|
|
||||
7 | foo a b Refl impossible
|
||||
| ~~~~~~~~~~
|
||||
foo a b Refl is a valid case
|
||||
|
||||
|
@ -3,23 +3,28 @@ totality021.idr:8:1-67:
|
||||
8 | sLevelNotSLevel' (SL (Delay level)) p = sLevelNotSLevel' level Refl
|
||||
| ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
Main.sLevelNotSLevel' is possibly not total due to recursive path Main.sLevelNotSLevel' --> Main.sLevelNotSLevel'
|
||||
|
||||
totality021.idr:12:1-66:
|
||||
|
|
||||
12 | sLevelNotSLevel (SL (Delay level)) p = sLevelNotSLevel' level Refl
|
||||
| ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
Main.sLevelNotSLevel is possibly not total due to: Main.sLevelNotSLevel'
|
||||
|
||||
totality021.idr:18:1-26:
|
||||
|
|
||||
18 | v = sLevelNotSLevel l Refl
|
||||
| ~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
Main.v is possibly not total due to: Main.sLevelNotSLevel
|
||||
|
||||
totality021a.idr:9:1-37:
|
||||
|
|
||||
9 | noNonEmptyPointInt {n} Nil impossible
|
||||
| ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
Main.noNonEmptyPointInt is not total as there are missing cases
|
||||
|
||||
totality021a.idr:12:1-31:
|
||||
|
|
||||
12 | myVoid = noNonEmptyPointInt [2]
|
||||
| ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
Main.myVoid is possibly not total due to: Main.noNonEmptyPointInt
|
||||
|
||||
|
@ -3,3 +3,4 @@ totality022.idr:7:20-29:
|
||||
7 | f _ [] (RSnoc _ _) impossible -- = ?wat
|
||||
| ~~~~~~~~~~
|
||||
f _ [] (RSnoc _ _) is a valid case
|
||||
|
||||
|
@ -3,3 +3,4 @@ totality023.idr:9:1-10:27:
|
||||
9 | run (Do x f) = do r <- x
|
||||
| ~~~~~~~~~~~~~~~~~~~~~~~~ ...
|
||||
Main.run is possibly not total due to recursive path Main.run --> Main.run
|
||||
|
||||
|
@ -3,13 +3,16 @@ tutorial002.idr:41:25-29:
|
||||
41 | Main.natToBin_lemma_1 = proof
|
||||
| ~~~~~
|
||||
This style of tactic proof is deprecated. See %runElab for the replacement.
|
||||
|
||||
tutorial002.idr:48:18-22:
|
||||
|
|
||||
48 | parity_lemma_1 = proof
|
||||
| ~~~~~
|
||||
This style of tactic proof is deprecated. See %runElab for the replacement.
|
||||
|
||||
tutorial002.idr:54:18-22:
|
||||
|
|
||||
54 | parity_lemma_2 = proof {
|
||||
| ~~~~~
|
||||
This style of tactic proof is deprecated. See %runElab for the replacement.
|
||||
|
||||
|
@ -3,8 +3,10 @@ tutorial004.idr:46:14-18:
|
||||
46 | plusredZ_S = proof {
|
||||
| ~~~~~
|
||||
This style of tactic proof is deprecated. See %runElab for the replacement.
|
||||
|
||||
tutorial004.idr:53:14-18:
|
||||
|
|
||||
53 | plusredZ_Z = proof {
|
||||
| ~~~~~
|
||||
This style of tactic proof is deprecated. See %runElab for the replacement.
|
||||
|
||||
|
@ -16,6 +16,7 @@ When checking argument xs to constructor Data.Vect.:::
|
||||
plus len len
|
||||
and
|
||||
plus len m
|
||||
|
||||
tutorial006b.idr:10:37-50:
|
||||
|
|
||||
10 | parity (S (S (j + j))) | Even = Even {n=S j}
|
||||
@ -33,3 +34,4 @@ Specifically:
|
||||
plus (S j) (S j)
|
||||
and
|
||||
S (S (plus j j))
|
||||
|
||||
|
@ -6,6 +6,7 @@ Type mismatch between
|
||||
Int -> String
|
||||
and
|
||||
UniqueType (Int -> String)
|
||||
|
||||
unique001a.idr:46:15-54:28:
|
||||
|
|
||||
46 | showStuff' xs = do
|
||||
@ -14,6 +15,7 @@ Type mismatch between
|
||||
Int -> String
|
||||
and
|
||||
UniqueType (Int -> String)
|
||||
|
||||
unique001a.idr:57:15-62:33:
|
||||
|
|
||||
57 | showThings xs = do
|
||||
@ -22,31 +24,37 @@ Type mismatch between
|
||||
UniqueType (Int -> String)
|
||||
and
|
||||
Int -> String
|
||||
|
||||
unique001b.idr:18:17-42:
|
||||
|
|
||||
18 | showU (x :: xs) = show x ++ "," ++ free xs
|
||||
| ~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
Borrowed name xs must not be used on RHS
|
||||
|
||||
unique001c.idr:47:12-62:
|
||||
|
|
||||
47 | ndup {a} x = (\f : Int -> a => MkUPair (f 0) (f 1)) (uconst x)
|
||||
| ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
Unique name f is used more than once
|
||||
|
||||
unique001d.idr:4:16-18:
|
||||
|
|
||||
4 | steal (Read x) = x
|
||||
| ~~~
|
||||
Borrowed name x must not be used on RHS
|
||||
|
||||
unique001e.idr:4:12-40:
|
||||
|
|
||||
4 | Nil : {a : UniqueType} -> BadList a
|
||||
| ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
Constructor Main.Nil has a UniqueType, but the data type does not
|
||||
|
||||
unique002.idr:17:8-20:19:
|
||||
|
|
||||
17 | foo xs = do -- let f = \x : Int => showU xs
|
||||
| ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...
|
||||
Unique name xs is used more than once
|
||||
|
||||
unique002a.idr:17:8-20:19:
|
||||
|
|
||||
17 | foo xs = do let f = \x : Int => showU xs
|
||||
@ -55,6 +63,7 @@ Type mismatch between
|
||||
Int -> String
|
||||
and
|
||||
UniqueType (Int -> String)
|
||||
|
||||
unique003.idr:20:8-24:19:
|
||||
|
|
||||
20 | foo xs = do let f = \x : Int => showU xs -- can't build this in unique context
|
||||
@ -63,3 +72,4 @@ Type mismatch between
|
||||
Int -> String
|
||||
and
|
||||
UniqueType (Int -> String)
|
||||
|
||||
|
@ -11,3 +11,4 @@ Universe inconsistency.
|
||||
ConstraintFC {uconstraint = ./universes001.idr.x < ./universes001.idr.y, ufc = universes001.idr:1:6-8}
|
||||
ConstraintFC {uconstraint = ./universes001.idr.z < ./universes001.idr.x, ufc = universes001.idr:1:6-8}
|
||||
ConstraintFC {uconstraint = ./universes001.idr.x <= ./universes001.idr.z, ufc = universes001.idr:7:5-21}
|
||||
|
||||
|
@ -11,3 +11,4 @@ Universe inconsistency.
|
||||
ConstraintFC {uconstraint = ./universes002.idr.b1 < ./universes002.idr.c1, ufc = universes002.idr:3:6-10}
|
||||
ConstraintFC {uconstraint = ./universes002.idr.b1 <= ./universes002.idr.e7, ufc = universes002.idr:45:9-48}
|
||||
ConstraintFC {uconstraint = ./universes002.idr.d1 <= ./universes002.idr.b1, ufc = universes002.idr:3:6-10}
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user