git.iko.soy/Idris-dev
on master help sign in
Put source code before error (like parse errors)
commit7d0c06b108bf3af9e23ae7e95c5f35970b61d7bc authorJason Felice <jason.m.felice@gmail.com> dateTue 5 Dec 2017, 21:54 (9 years ago) parent0bb18f1
66 files changed+453−333
compare with master
unifiedsplit
src/Idris/Output.hs+11−5 test/basic002/expected+2−2 test/basic006/expected+5−4 test/basic009/expected+10−7 test/basic016/expected+1−1 test/basic017/expected+4−3 test/basic018/expected+8−7 test/directives001/expected+14−8 test/directives002/expected+1−1 test/effects003/expected+1−1 test/error001/expected+5−4 test/error003/expected+3−3 test/error004/expected+6−6 test/error005/expected+21−16 test/error006/expected+3−2 test/error007/expected+3−3 test/error008/expected+5−3 test/ffi002/expected+2−1 test/interfaces008/expected+1−1 test/layout001/expected+5−4 test/literate001/expected+2−1 test/meta002/expected+8−8 test/meta003/expected+3−3 test/meta004/expected+2−2 test/proof001/expected+2−2 test/proof002/expected+6−6 test/proof003/expected+6−6 test/proof007/expected+3−3 test/proof008/expected+1−1 test/proof011/expected+6−6 test/quasiquote003/expected+5−4 test/quasiquote004/expected+6−6 test/quasiquote006/expected+10−10 test/reg017/expected+2−2 test/reg027/expected+2−1 test/regression002/expected+108−78 test/sourceLocation001/expected+4−4 test/syntax001/expected+8−6 test/totality001/expected+6−3 test/totality002/expected+4−3 test/totality003/expected+1−1 test/totality004/expected+3−2 test/totality006/expected+5−3 test/totality007/expected+1−1 test/totality008/expected+2−1 test/totality009/expected+20−10 test/totality010/expected+4−2 test/totality011/expected+1−1 test/totality012/expected+2−2 test/totality013/expected+3−2 test/totality014/expected+5−4 test/totality015/expected+5−3 test/totality016/expected+18−9 test/totality017/expected+12−6 test/totality018/expected+2−1 test/totality019/expected+4−2 test/totality020/expected+4−2 test/totality021/expected+5−5 test/totality022/expected+2−1 test/totality023/expected+1−1 test/tutorial002/expected+3−3 test/tutorial004/expected+2−2 test/tutorial006/expected+6−6 test/unique004/expected+27−18 test/universes001/expected+5−4 test/universes002/expected+5−4
src/Idris/Output.hs+11−5
@@ -82,18 +82,24 @@ iWarn fc err =
8282 case idris_outputmode i of
8383 RawOutput h ->
8484 do maybeSource <- readSource fc
85− let maybeFormattedSource = maybeSource >>= formatWarning fc
85+ let maybeFormattedSource = (maybeSource >>= formatWarning fc)
8686 err' <- iRender . fmap (fancifyAnnots i True) $
87− (case fc of
88− FC fn _ _ | fn /= "" -> text (show fc) <> colon <//> err
89− _ -> err) <>
90− string (maybe "" ("\n" ++) maybeFormattedSource)
87+ layoutError (formatFC fc) (fmap string maybeFormattedSource) err
9188 hWriteDoc h i err'
9289 IdeMode n h ->
9390 do err' <- iRender . fmap (fancifyAnnots i True) $ err
9491 let (str, spans) = displaySpans err'
9592 runIO . hPutStrLn h $
9693 convSExp "warning" (fc_fname fc, fc_start fc, fc_end fc, str, spans) n
94+ where
95+ formatFC :: FC -> Doc OutputAnnotation
96+ formatFC (FC fn _ _) | fn /= "" = text (show fc) <> colon
97+ formatFC _ = empty
98+
99+ layoutError :: Doc OutputAnnotation -> Maybe (Doc OutputAnnotation) -> Doc OutputAnnotation -> Doc OutputAnnotation
100+ layoutError loc (Just src) err = loc <$$> src <$$> err
101+ layoutError loc Nothing err = loc </> err
102+
97103
98104iRender :: Doc a -> Idris (SimpleDoc a)
99105iRender d = do w <- getWidth
test/basic002/expected+2−2
@@ -1,11 +1,11 @@
11test006.idr:25:23-27:
2−This style of tactic proof is deprecated. See %runElab for the replacement.
32 |
4325 | Main.parity_lemma_2 = proof {
54 | ~~~~~
6−test006.idr:32:23-27:
75This style of tactic proof is deprecated. See %runElab for the replacement.
6+test006.idr:32:23-27:
87 |
9832 | Main.parity_lemma_1 = proof {
109 | ~~~~~
10+This style of tactic proof is deprecated. See %runElab for the replacement.
1111[False, True, False, True, False, True]
test/basic006/expected+5−4
@@ -1,4 +1,8 @@
1−test020a.idr:16:10-19:When checking right hand side of foo with expected type
1+test020a.idr:16:10-19:
2+ |
3+16 | foo xs = reverse xs
4+ | ~~~~~~~~~~
5+When checking right hand side of foo with expected type
26 List a
37
48When checking an application of function Prelude.List.reverse:
@@ -6,8 +10,5 @@ When checking an application of function Prelude.List.reverse:
610 Vect n a (Type of xs)
711 and
812 List a (Expected type)
9− |
10−16 | foo xs = reverse xs
11− | ~~~~~~~~~~
1213[3, 2, 1]
1314"Number 42"
test/basic009/expected+10−7
@@ -1,10 +1,15 @@
11MAIN-PASS
2−Faulty.idr:6:9-11:num is bound as an implicit
3− Did you mean to refer to A.num?
2+Faulty.idr:6:9-11:
43 |
546 | fault : num = Z
65 | ~~~
7−Faulty.idr:7:7-12:When checking right hand side of fault with expected type
6+num is bound as an implicit
7+ Did you mean to refer to A.num?
8+Faulty.idr:7:7-12:
9+ |
10+7 | fault = Refl
11+ | ~~~~~~
12+When checking right hand side of fault with expected type
813 num = 0
914
1015Type mismatch between
@@ -17,10 +22,8 @@ Specifically:
1722 0
1823 and
1924 num
20− |
21−7 | fault = Refl
22− | ~~~~~~
23−Multiple.idr:3:21:import alias not unique: "X"
25+Multiple.idr:3:21:
2426 |
25273 | import Data.Vect as X
2628 | ^
29+import alias not unique: "X"
test/basic016/expected+1−1
@@ -1 +1 @@
1−Cycle detected in imports: CycleA.idr -> CycleB -> CycleC -> CycleA -> CycleB
1+ Cycle detected in imports: CycleA.idr -> CycleB -> CycleC -> CycleA -> CycleB
test/basic017/expected+4−3
@@ -1,6 +1,7 @@
1−basic017a.idr:11:8:When checking type of Main.append:
2−When checking an application of Main.Vect:
3− No such variable n
1+basic017a.idr:11:8:
42 |
5311 | append : Vect n a -> Vect m a -> Vect (n + m) a
64 | ^
5+When checking type of Main.append:
6+When checking an application of Main.Vect:
7+ No such variable n
test/basic018/expected+8−7
@@ -1,16 +1,20 @@
11basic018.idr:7:12-16:
2−thing is bound as an implicit
3− Did you mean to refer to Main.thing?
42 |
537 | Vect thing elem
64 | ~~~~~
7−basic018.idr:12:8-12:
85thing is bound as an implicit
96 Did you mean to refer to Main.thing?
7+basic018.idr:12:8-12:
108 |
11912 | test : thing = S 41
1210 | ~~~~~
13−basic018.idr:13:6-11:When checking right hand side of test with expected type
11+thing is bound as an implicit
12+ Did you mean to refer to Main.thing?
13+basic018.idr:13:6-11:
14+ |
15+13 | test = Refl
16+ | ~~~~~~
17+When checking right hand side of test with expected type
1418 thing = S 41
1519
1620Type mismatch between
@@ -23,6 +27,3 @@ Specifically:
2327 42
2428 and
2529 thing
26− |
27−13 | test = Refl
28− | ~~~~~~
test/directives001/expected+14−8
@@ -1,30 +1,36 @@
1−directives001.idr:14:7:Use of deprecated name directives001.Foo
2−To be replaced with `Bar`.
1+directives001.idr:14:7:
32 |
4314 | mkFoo : String -> Foo
54 | ^
6−directives001.idr:14:7:Use of deprecated name directives001.Foo
5+Use of deprecated name directives001.Foo
76To be replaced with `Bar`.
7+directives001.idr:14:7:
88 |
9914 | mkFoo : String -> Foo
1010 | ^
11−directives001.idr:15:7-13:Use of deprecated name directives001.Foo
11+Use of deprecated name directives001.Foo
1212To be replaced with `Bar`.
13+directives001.idr:15:7-13:
1314 |
141515 | mkFoo = MkFoo
1516 | ~~~~~~~
16−directives001.idr:15:7-13:Use of deprecated name directives001.Foo
17+Use of deprecated name directives001.Foo
1718To be replaced with `Bar`.
19+directives001.idr:15:7-13:
1820 |
192115 | mkFoo = MkFoo
2022 | ~~~~~~~
21−directives001.idr:26:8-28:28:Use of a fragile construct directives001.mkBar
22−How `Bar`s are to be created is still being discussed, `mkBar` is subject to change.
23+Use of deprecated name directives001.Foo
24+To be replaced with `Bar`.
25+directives001.idr:26:8-28:28:
2326 |
242726 | main = do
2528 | ~~~~ ...
26−directives001.idr:26:8-28:28:Use of a fragile construct directives001.mkBar
29+Use of a fragile construct directives001.mkBar
2730How `Bar`s are to be created is still being discussed, `mkBar` is subject to change.
31+directives001.idr:26:8-28:28:
2832 |
293326 | main = do
3034 | ~~~~ ...
35+Use of a fragile construct directives001.mkBar
36+How `Bar`s are to be created is still being discussed, `mkBar` is subject to change.
test/directives002/expected+1−1
@@ -1,5 +1,5 @@
11directives002.idr:12:3-14:28:
2−directives002.Main.main is possibly not total due to: directives002.loop
32 |
4312 | main = do
54 | ~~~~~~~~~ ...
5+directives002.Main.main is possibly not total due to: directives002.loop
test/effects003/expected+1−1
@@ -1,8 +1,8 @@
11hangman.idr:204:8-12:
2−This style of tactic proof is deprecated. See %runElab for the replacement.
32 |
43204 | wlen = proof search
54 | ~~~~~
5+This style of tactic proof is deprecated. See %runElab for the replacement.
66------------
77
886 guesses left
test/error001/expected+5−4
@@ -1,4 +1,8 @@
1−test002.idr:1:6:Universe inconsistency.
1+test002.idr:1:6:
2+ |
3+1 | myid : (a : Type) -> a -> a
4+ | ^
5+Universe inconsistency.
26 Working on: ./test002.idr.z
37 Old domain: (6,6)
48 New domain: (6,5)
@@ -6,6 +10,3 @@ test002.idr:1:6:Universe inconsistency.
610 ConstraintFC {uconstraint = ./test002.idr.z <= ./test002.idr.a1, ufc = test002.idr:1:6}
711 ConstraintFC {uconstraint = ./test002.idr.y < ./test002.idr.z, ufc = test002.idr:1:6}
812 ConstraintFC {uconstraint = ./test002.idr.z <= ./test002.idr.a1, ufc = test002.idr:1:6}
9− |
10−1 | myid : (a : Type) -> a -> a
11− | ^
test/error003/expected+3−3
@@ -1,8 +1,8 @@
11ErrorReflection.idr:68:5-20:
2+ |
3+68 | bad = Lam (Var Here)
4+ | ~~~~~~~~~~~~~~~~
25When checking right hand side of bad with expected type
36 Tm [] TUnit
47
58DSL type error: (t(504) => t'(503)) doesn't match ()
6− |
7−68 | bad = Lam (Var Here)
8− | ~~~~~~~~~~~~~~~~
test/error004/expected+6−6
@@ -1,18 +1,18 @@
11FunErrTest.idr:35:12-18:
2+ |
3+35 | badCadr1 = cadr []
4+ | ~~~~~~~
25When checking right hand side of badCadr1 with expected type
36 Int
47
58When checking argument cons2 to function FunErrTest.cadr:
69 Could not prove that [] has at least two elements.
7− |
8−35 | badCadr1 = cadr []
9− | ~~~~~~~
1010FunErrTest.idr:38:12-19:
11+ |
12+38 | badCadr2 = cadr [1]
13+ | ~~~~~~~~
1114When checking right hand side of badCadr2 with expected type
1215 Int
1316
1417When checking argument cons2 to function FunErrTest.cadr:
1518 Could not prove that [] has at least two elements.
16− |
17−38 | badCadr2 = cadr [1]
18− | ~~~~~~~~
test/error005/expected+21−16
@@ -1,46 +1,51 @@
1−error005.idr:11:7:When checking right hand side of two with expected type
1+error005.idr:11:7:
2+ |
3+11 | two = 2
4+ | ^
5+When checking right hand side of two with expected type
26 Fin 2
37
48When checking argument prf to function Data.Fin.fromInteger:
59 When using 2 as a literal for a Fin 2
610 2 is not strictly less than 2
11+error005.idr:14:12:
712 |
8−11 | two = 2
9− | ^
10−error005.idr:14:12:When checking right hand side of hahaha with expected type
13+14 | hahaha n = 0
14+ | ^
15+When checking right hand side of hahaha with expected type
1116 Fin n
1217
1318When checking argument prf to function Data.Fin.fromInteger:
1419 When using 0 as a literal for a Fin n
1520 0 is not strictly less than n
21+error005.idr:20:11:
1622 |
17−14 | hahaha n = 0
18− | ^
19−error005.idr:20:11:When checking right hand side of notOk with expected type
23+20 | notOk n = 2
24+ | ^
25+When checking right hand side of notOk with expected type
2026 Fin (plus 2 n)
2127
2228When checking argument prf to function Data.Fin.fromInteger:
2329 When using 2 as a literal for a Fin (S (S n))
2430 2 is not strictly less than S (S n)
31+error005.idr:23:12-24:
2532 |
26−20 | notOk n = 2
27− | ^
28−error005.idr:23:12-24:When checking right hand side of b0rken with expected type
33+23 | b0rken n = fromInteger n
34+ | ~~~~~~~~~~~~~
35+When checking right hand side of b0rken with expected type
2936 Fin 3
3037
3138When checking argument prf to function Data.Fin.fromInteger:
3239 When using n as a literal for a Fin 3
3340 Could not show that n is less than 3 because n is a bound
3441 variable instead of a constant Integer
42+error005.idr:26:17:
3543 |
36−23 | b0rken n = fromInteger n
37− | ~~~~~~~~~~~~~
38−error005.idr:26:17:When checking right hand side of x with expected type
44+26 | x = the (Fin 4) 5
45+ | ^
46+When checking right hand side of x with expected type
3947 Fin 4
4048
4149When checking argument prf to function Data.Fin.fromInteger:
4250 When using 5 as a literal for a Fin 4
4351 5 is not strictly less than 4
44− |
45−26 | x = the (Fin 4) 5
46− | ^
test/error006/expected+3−2
@@ -1,5 +1,6 @@
1−WithPatsNoWith.idr:4:1-13:When checking left hand side of foo:
2−unexpected patterns outside of "with" block
1+WithPatsNoWith.idr:4:1-13:
32 |
434 | foo 1 | 2 | 3 = True
54 | ~~~~~~~~~~~~~
5+When checking left hand side of foo:
6+unexpected patterns outside of "with" block
test/error007/expected+3−3
@@ -1,4 +1,7 @@
11error007.idr:26:7-29:
2+ |
3+26 | send_page conn str code -- (prim__zextB32_Int code)
4+ | ~~~~~~~~~~~~~~~~~~~~~~~
25When checking right hand side of answer_to_connection with expected type
36 IO Int
47
@@ -13,6 +16,3 @@ When checking argument code to function Main.send_page:
1316 Bits32
1417 and
1518 Int
16− |
17−26 | send_page conn str code -- (prim__zextB32_Int code)
18− | ~~~~~~~~~~~~~~~~~~~~~~~
test/error008/expected+5−3
@@ -1,10 +1,12 @@
1−error008.idr:3:4:When checking type of Main.s2:
2−Can't disambiguate name: Prelude.List.Nil, Data.Vect.Nil
1+error008.idr:3:4:
32 |
433 | s2 : x + sum Nil = x * fromInteger 0
54 | ^
6−error008a.idr:3:4:When checking type of Main.s1:
5+When checking type of Main.s2:
76Can't disambiguate name: Prelude.List.Nil, Data.Vect.Nil
7+error008a.idr:3:4:
88 |
993 | s1 : Num a => {x : a} -> x + sum {a} Nil = x -- * fromInteger 0
1010 | ^
11+When checking type of Main.s1:
12+Can't disambiguate name: Prelude.List.Nil, Data.Vect.Nil
test/ffi002/expected+2−1
@@ -1,4 +1,5 @@
1−test023.idr:20:26-36:Type provider error: Always fails
1+test023.idr:20:26-36:
22 |
3320 | %provide (t : Type) with badProvider
44 | ~~~~~~~~~~~
5+Type provider error: Always fails
test/interfaces008/expected+1−1
@@ -1,5 +1,5 @@
11interfaces008.idr:20:18-23:
2−Default implementations must be for a super interface constraint on the containing interface.
32 |
4320 | implementation Foo2 a where
54 | ~~~~~~
5+Default implementations must be for a super interface constraint on the containing interface.
test/layout001/expected+5−4
@@ -58,14 +58,15 @@ Wrong indention: should be greater than context indentation
5858 | ^
5959Wrong indention: should be greater than context indentation
6060
61−mplus1.idr:13:31-17:49:When checking right hand side of term with expected type
61+mplus1.idr:13:31-17:49:
62+ |
63+13 | term = do f <- factor
64+ | ~~~~~~~~~~~~~~~~~ ...
65+When checking right hand side of term with expected type
6266 Maybe Int
6367
6468When checking an application of function Prelude.Applicative.pure:
6569 No such variable f
66− |
67−13 | term = do f <- factor
68− | ~~~~~~~~~~~~~~~~~ ...
6970./mplus2.idr:17:37:
7071 |
717217 | `mplus` pure f
test/literate001/expected+2−1
@@ -1,7 +1,8 @@
1−./test003a.lidr:1:0:Program line next to comment
1+./test003a.lidr:1:0:
22 |
331 | Broken
44 | ^
5+Program line next to comment
56'a'
67'd'
78zabcdefg
test/meta002/expected+8−8
@@ -1,22 +1,22 @@
11DataDef.idr:74:1-8:
2−While running an elaboration script, the following error occurred:
3−Prelude.Either.Either is already defined as a datatype.
42 |
5374 | %runElab nope
64 | ~~~~~~~~
5+While running an elaboration script, the following error occurred:
6+Prelude.Either.Either is already defined as a datatype.
77Tacs.idr:299:15-300:78:
8+ |
9+299 | testElab3 = %runElab (elaborateSTLC (App (Lam "x" (App (Var 0) (Var 0)))
10+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...
811When checking right hand side of testElab3 with expected type
912 DPair Ty (Tm [])
1013
1114Unifying ty and ARR ty t would lead to infinite value
12− |
13−299 | testElab3 = %runElab (elaborateSTLC (App (Lam "x" (App (Var 0) (Var 0)))
14− | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...
1515AgdaStyleReflection.idr:315:5-20:
16+ |
17+315 | baz = tactic trivial
18+ | ~~~~~~~~~~~~~~~~
1619When checking right hand side of baz with expected type
1720 (Nat, Void)
1821
1922PROOF SEARCH FAILURE is not defined.
20− |
21−315 | baz = tactic trivial
22− | ~~~~~~~~~~~~~~~~
test/meta003/expected+3−3
@@ -1,9 +1,9 @@
11BadDef.idr:14:1-8:
2+ |
3+14 | %runElab mkBadDef1
4+ | ~~~~~~~~
25While running an elaboration script, the following error occurred:
36Type mismatch between
47 ()
58and
69 String
7− |
8−14 | %runElab mkBadDef1
9− | ~~~~~~~~
test/meta004/expected+2−2
@@ -1,6 +1,6 @@
11meta004.idr:50:1-8:
2−While running an elaboration script, the following error occurred:
3−Not an impossible case
42 |
5350 | %runElab domore
64 | ~~~~~~~~
5+While running an elaboration script, the following error occurred:
6+Not an impossible case
test/proof001/expected+2−2
@@ -1,10 +1,10 @@
11test029.idr:29:25-29:
2−This style of tactic proof is deprecated. See %runElab for the replacement.
32 |
4329 | simple.append_lemma_2 = proof {
54 | ~~~~~
6−test029.idr:36:25-29:
75This style of tactic proof is deprecated. See %runElab for the replacement.
6+test029.idr:36:25-29:
87 |
9836 | simple.append_lemma_1 = proof {
109 | ~~~~~
10+This style of tactic proof is deprecated. See %runElab for the replacement.
test/proof002/expected+6−6
@@ -1,19 +1,22 @@
11Reflect.idr:175:21-25:
2−This style of tactic proof is deprecated. See %runElab for the replacement.
32 |
43175 | Reflect.appRExpr1 = proof {
54 | ~~~~~
6−Reflect.idr:184:21-25:
75This style of tactic proof is deprecated. See %runElab for the replacement.
6+Reflect.idr:184:21-25:
87 |
98184 | Reflect.appRExpr2 = proof {
109 | ~~~~~
11−Reflect.idr:192:15-19:
1210This style of tactic proof is deprecated. See %runElab for the replacement.
11+Reflect.idr:192:15-19:
1312 |
1413192 | Reflect.bp1 = proof {
1514 | ~~~~~
15+This style of tactic proof is deprecated. See %runElab for the replacement.
1616test030a.idr:12:26-37:
17+ |
18+12 | testReflect1 {a} xs ys = AssocProof a
19+ | ~~~~~~~~~~~~
1720When checking right hand side of testReflect1 with expected type
1821 ys ++ x :: ys ++ xs = (xs ++ [x]) ++ ys ++ xs
1922
@@ -28,6 +31,3 @@ When checking an application of function Reflect.getJust:
2831 Just x
2932 and
3033 Nothing
31− |
32−12 | testReflect1 {a} xs ys = AssocProof a
33− | ~~~~~~~~~~~~
test/proof003/expected+6−6
@@ -1,33 +1,33 @@
11Parity.idr:17:18-22:
2−This style of tactic proof is deprecated. See %runElab for the replacement.
32 |
4317 | parity_lemma_2 = proof {
54 | ~~~~~
6−Parity.idr:24:18-22:
75This style of tactic proof is deprecated. See %runElab for the replacement.
6+Parity.idr:24:18-22:
87 |
9824 | parity_lemma_1 = proof {
109 | ~~~~~
11−test015.idr:88:15-19:
1210This style of tactic proof is deprecated. See %runElab for the replacement.
11+test015.idr:88:15-19:
1312 |
141388 | Main.ntbOdd = proof {
1514 | ~~~~~
16−test015.idr:97:16-20:
1715This style of tactic proof is deprecated. See %runElab for the replacement.
16+test015.idr:97:16-20:
1817 |
191897 | Main.ntbEven = proof {
2019 | ~~~~~
21−test015.idr:107:20-24:
2220This style of tactic proof is deprecated. See %runElab for the replacement.
21+test015.idr:107:20-24:
2322 |
2423107 | Main.adc_lemma_2 = proof {
2524 | ~~~~~
26−test015.idr:142:20-24:
2725This style of tactic proof is deprecated. See %runElab for the replacement.
26+test015.idr:142:20-24:
2827 |
2928142 | Main.adc_lemma_1 = proof {
3029 | ~~~~~
30+This style of tactic proof is deprecated. See %runElab for the replacement.
313100101010
323201011001
3333010000011
test/proof007/expected+3−3
@@ -1,9 +1,9 @@
11DefaultArgUnknownName.idr:9:6-23:
2+ |
3+9 | test = funWithBadDefArg
4+ | ~~~~~~~~~~~~~~~~~~
25When checking right hand side of test with expected type
36 ()
47
58When checking argument arg to function DefaultArgUnknownName.funWithBadDefArg:
69 No such variable sadgjhsag
7− |
8−9 | test = funWithBadDefArg
9− | ~~~~~~~~~~~~~~~~~~
test/proof008/expected+1−1
@@ -1,5 +1,5 @@
11ClaimAndUnfocus.idr:8:27-31:
2−This style of tactic proof is deprecated. See %runElab for the replacement.
32 |
438 | ClaimAndUnfocus.foo_rhs = proof
54 | ~~~~~
5+This style of tactic proof is deprecated. See %runElab for the replacement.
test/proof011/expected+6−6
@@ -1,4 +1,7 @@
11proof011.idr:20:5-21:18:
2+ |
3+20 | = rewrite vassoc xs ys xs using vreplace in
4+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...
25When checking right hand side of vassoc' with expected type
36 (x :: xs) ++ ys ++ zs = ((x :: xs) ++ ys) ++ zs
47
@@ -8,10 +11,10 @@ rewriting xs ++ ys ++ xs to (xs ++ ys) ++ xs did not change type x ::
811 x ::
912 (xs ++ ys) ++
1013 zs
11− |
12−20 | = rewrite vassoc xs ys xs using vreplace in
13− | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...
1414proof011a.idr:14:5-37:
15+ |
16+14 | = rewrite vassoc xs ys xs in Refl
17+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1518When checking right hand side of vassoc' with expected type
1619 (x :: xs) ++ ys ++ zs = ((x :: xs) ++ ys) ++ zs
1720
@@ -21,6 +24,3 @@ rewriting xs ++ ys ++ xs to (xs ++ ys) ++ xs did not change type x ::
2124 x ::
2225 (xs ++ ys) ++
2326 zs
24− |
25−14 | = rewrite vassoc xs ys xs in Refl
26− | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
test/quasiquote003/expected+5−4
@@ -1,7 +1,8 @@
1−NoInfer.idr:11:5-11:When checking right hand side of zzz with expected type
2− TT
3−
4−No such variable k
1+NoInfer.idr:11:5-11:
52 |
6311 | zzz = `(FZ)
74 | ~~~~~~~
5+When checking right hand side of zzz with expected type
6+ TT
7+
8+No such variable k
test/quasiquote004/expected+6−6
@@ -1,23 +1,23 @@
11Quasiquote004.idr:39:26-30:
2−This style of tactic proof is deprecated. See %runElab for the replacement.
32 |
4339 | Quasiquote004.getMeNat = proof
54 | ~~~~~
6−Quasiquote004.idr:42:28-32:
75This style of tactic proof is deprecated. See %runElab for the replacement.
6+Quasiquote004.idr:42:28-32:
87 |
9842 | Quasiquote004.fizzyIsAOK = proof
109 | ~~~~~
11−Quasiquote004.idr:50:27-31:
1210This style of tactic proof is deprecated. See %runElab for the replacement.
11+Quasiquote004.idr:50:27-31:
1312 |
141350 | Quasiquote004.getMeNat' = proof
1514 | ~~~~~
15+This style of tactic proof is deprecated. See %runElab for the replacement.
1616Quasiquote004.idr:50:25-51:18:
17+ |
18+50 | Quasiquote004.getMeNat' = proof
19+ | ~~~~~~~ ...
1720When checking right hand side of Quasiquote004.getMeNat' with expected type
1821 String
1922
2023Not a Nat goal
21− |
22−50 | Quasiquote004.getMeNat' = proof
23− | ~~~~~~~ ...
test/quasiquote006/expected+10−10
@@ -1,28 +1,28 @@
11quasiquote006.idr:9:3-10:
2+ |
3+9 | b = `{Nil}
4+ | ~~~~~~~~
25When checking right hand side of b with expected type
36 TTName
47
58Can't disambiguate name: ForeignEnv.Nil,
69 Prelude.List.Nil
7− |
8−9 | b = `{Nil}
9− | ~~~~~~~~
1010quasiquote006.idr:12:3-17:
11+ |
12+12 | c = `{alsdkjflkj}
13+ | ~~~~~~~~~~~~~~~
1114When checking right hand side of c with expected type
1215 TTName
1316
1417No such variable alsdkjflkj
15− |
16−12 | c = `{alsdkjflkj}
17− | ~~~~~~~~~~~~~~~
1818quasiquote006.idr:15:3-11:
19+ |
20+15 | d = `{(::)}
21+ | ~~~~~~~~~
1922When checking right hand side of d with expected type
2023 TTName
2124
2225Can't disambiguate name: ForeignEnv.::,
2326 Prelude.List.::,
2427 Prelude.Stream.::
25− |
26−15 | d = `{(::)}
27− | ~~~~~~~~~
28−quasiquote006.idr:17:3:Main.d already defined
28+ quasiquote006.idr:17:3:Main.d already defined
test/reg017/expected+2−2
@@ -1,11 +1,11 @@
11reg017.idr:5:17-23:
2−This style of tactic proof is deprecated. See %runElab for the replacement.
32 |
435 | { default tactics { refine Refl; solve; } prfA : a = a } ->
54 | ~~~~~~~
6−reg017.idr:8:17-23:
75This style of tactic proof is deprecated. See %runElab for the replacement.
6+reg017.idr:8:17-23:
87 |
988 | { default tactics { refine Refl; solve; } prfBC : b = c } ->
109 | ~~~~~~~
10+This style of tactic proof is deprecated. See %runElab for the replacement.
11114
test/reg027/expected+2−1
@@ -1,5 +1,6 @@
11<<int fn>>
2−reg027a.idr:9:16-30:Overlapping implementation: Show (Int -> a) already defined
2+reg027a.idr:9:16-30:
33 |
449 | implementation Show (Int -> b) where
55 | ~~~~~~~~~~~~~~~
6+Overlapping implementation: Show (Int -> a) already defined
test/regression002/expected+108−78
@@ -1,28 +1,36 @@
1−reg003a.idr:4:13-38:When checking type of Main.ECons:
2−No such variable OddList
1+reg003a.idr:4:13-38:
32 |
434 | ECons : Nat -> OddList -> EvenList
54 | ~~~~~~~~~~~~~~~~~~~~~~~~~~
6−reg003a.idr:7:13-38:When checking type of Main.OCons:
7−No such variable EvenList
5+When checking type of Main.ECons:
6+No such variable OddList
7+reg003a.idr:7:13-38:
88 |
997 | OCons : Nat -> EvenList -> OddList
1010 | ~~~~~~~~~~~~~~~~~~~~~~~~~~
11−reg003a.idr:9:6:When checking type of Main.test:
11+When checking type of Main.OCons:
1212No such variable EvenList
13+reg003a.idr:9:6:
1314 |
14159 | test : EvenList
1516 | ^
17+When checking type of Main.test:
18+No such variable EvenList
1619reg006.idr:17:1-23:
17−RBTree.lookup is possibly not total due to recursive path RBTree.lookup --> RBTree.lookup
1820 |
192117 | lookup k Leaf = Nothing
2022 | ~~~~~~~~~~~~~~~~~~~~~~~
21−reg007.lidr:8:3-13:A.n is already defined
23+RBTree.lookup is possibly not total due to recursive path RBTree.lookup --> RBTree.lookup
24+reg007.lidr:8:3-13:
2225 |
23268 | > A.n = Z -- This is where it's at!
2427 | ~~~~~~~~~~~
25−reg007.lidr:12:13-18:When checking right hand side of hurrah with expected type
28+A.n is already defined
29+reg007.lidr:12:13-18:
30+ |
31+12 | > hurrah = isSame
32+ | ~~~~~~
33+When checking right hand side of hurrah with expected type
2634 0 = 1
2735
2836Type mismatch between
@@ -35,88 +43,95 @@ Specifically:
3543 1
3644 and
3745 0
38− |
39−12 | > hurrah = isSame
40− | ~~~~~~
4146reg010.idr:5:3-26:
42−When checking left hand side of with block in usubst.unsafeSubst:
43−Can't match on with block in usubst.unsafeSubst warg a P x x px
4447 |
45485 | unsafeSubst P x x px | _ = px
4649 | ~~~~~~~~~~~~~~~~~~~~~~~~
50+When checking left hand side of with block in usubst.unsafeSubst:
51+Can't match on with block in usubst.unsafeSubst warg a P x x px
4752reg018a.idr:16:1-18:
48−conat.minusCoNat is possibly not total due to recursive path conat.minusCoNat --> conat.minusCoNat
4953 |
505416 | minusCoNat Z n = Z
5155 | ~~~~~~~~~~~~~~~~~~
56+conat.minusCoNat is possibly not total due to recursive path conat.minusCoNat --> conat.minusCoNat
5257reg018a.idr:21:1-42:
53−conat.loopForever is possibly not total due to: conat.minusCoNat
5458 |
555921 | loopForever = minusCoNat infinity infinity
5660 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
61+conat.loopForever is possibly not total due to: conat.minusCoNat
5762reg018b.idr:8:1-28:
58−A.showB is possibly not total due to recursive path A.showB --> A.showB
5963 |
60648 | showB (I x) = "I" ++ showB x
6165 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
66+A.showB is possibly not total due to recursive path A.showB --> A.showB
6267reg018b.idr:11:1-6:
63−A.B implementation of Prelude.Show.Show is possibly not total due to: A.showB
6468 |
656911 | Show B where show = showB
6670 | ~~~~~~
71+A.B implementation of Prelude.Show.Show is possibly not total due to: A.showB
6772reg018c.idr:21:1-22:21:
68−CodataTest.inf is possibly not total due to: with block in CodataTest.inf
6973 |
707421 | inf (x :: xs) with (hdtl xs)
7175 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...
72−reg018d.idr:8:1-39:Main.pull is not total as there are missing cases
76+CodataTest.inf is possibly not total due to: with block in CodataTest.inf
77+reg018d.idr:8:1-39:
7378 |
74798 | pull {n=Z} _ (x :: xs) = (x, xs)
7580 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
76−reg023.idr:7:5-7:When checking right hand side of bad with expected type
81+Main.pull is not total as there are missing cases
82+reg023.idr:7:5-7:
83+ |
84+7 | bad = Z
85+ | ~~~
86+When checking right hand side of bad with expected type
7787 f Nat
7888
7989Type mismatch between
8090 Nat (Type of 0)
8191and
8292 f Nat (Expected type)
83− |
84−7 | bad = Z
85− | ~~~
86−reg028.idr:5:1-9:tbad.bad is possibly not total due to: with block in tbad.bad
93+reg028.idr:5:1-9:
8794 |
88955 | bad Z = Z
8996 | ~~~~~~~~~
97+tbad.bad is possibly not total due to: with block in tbad.bad
9098reg028a.idr:17:14-18:
91−This style of tactic proof is deprecated. See %runElab for the replacement.
9299 |
9310017 | qsortLemma = proof
94101 | ~~~~~
102+This style of tactic proof is deprecated. See %runElab for the replacement.
95103reg028a.idr:11:1-14:
96−tbad.qsort' is possibly not total due to: with block in tbad.qsort'
97104 |
9810511 | qsort' [] = []
99106 | ~~~~~~~~~~~~~~
100−reg034.idr:6:1-14:When checking left hand side of bar:
101−Can't match on bar xs xs Refl
107+tbad.qsort' is possibly not total due to: with block in tbad.qsort'
108+reg034.idr:6:1-14:
102109 |
1031106 | bar xs xs Refl = Refl
104111 | ~~~~~~~~~~~~~~
105−reg034.idr:9:1-14:When checking left hand side of foo:
106−Can't match on foo f x x Refl
112+When checking left hand side of bar:
113+Can't match on bar xs xs Refl
114+reg034.idr:9:1-14:
107115 |
1081169 | foo f x x Refl = Refl
109117 | ~~~~~~~~~~~~~~
110−reg035b.idr:8:12-38:No such variable __pi_arg
118+When checking left hand side of foo:
119+Can't match on foo f x x Refl
120+reg035b.idr:8:12-38:
111121 |
1121228 | fins Z = ([] ** (finZEmpty {a=_}))
113123 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~
124+No such variable __pi_arg
114125reg044.idr:4:6-10:
115−This style of tactic proof is deprecated. See %runElab for the replacement.
116126 |
1171274 | pf = proof
118128 | ~~~~~
119−reg044.idr:4:4-6:13:When checking right hand side of Main.pf with expected type
129+This style of tactic proof is deprecated. See %runElab for the replacement.
130+reg044.idr:4:4-6:13:
131+ |
132+4 | pf = proof
133+ | ~~~~~~~ ...
134+When checking right hand side of Main.pf with expected type
120135 (b : Nat) -> (a : Nat) -> (S a = S b) -> a = b
121136
122137Type mismatch between
@@ -129,21 +144,20 @@ Specifically:
129144 b
130145 and
131146 a
132− |
133−4 | pf = proof
134− | ~~~~~~~ ...
135−reg049.idr:2:11-14:When checking constructor Main.Bogus:
136−Void is not Main.Foo
147+reg049.idr:2:11-14:
137148 |
1381492 | Bogus : Void
139150 | ~~~~
140−reg049.idr:5:6-12:When checking right hand side of uhOh with expected type
141− Void
142−
143−No such variable Bogus
151+When checking constructor Main.Bogus:
152+Void is not Main.Foo
153+reg049.idr:5:6-12:
144154 |
1451555 | uhOh = Bogus
146156 | ~~~~~~~
157+When checking right hand side of uhOh with expected type
158+ Void
159+
160+No such variable Bogus
147161./badbangop.idr:7:1:
148162 |
1491637 | (!) : List a -> Nat -> Maybe a
@@ -156,90 +170,104 @@ No such variable Bogus
156170 | ^
157171unexpected Operator without known fixity: !!
158172
159−reg054.idr:18:1-17:When checking left hand side of inf:
160−When checking an application of constructor Main.MkInfer:
161− Attempting concrete match on polymorphic argument: 0
173+reg054.idr:18:1-17:
162174 |
16317518 | inf (MkInfer _ Z) = True
164176 | ~~~~~~~~~~~~~~~~~
165−reg054.idr:34:1-18:When checking left hand side of weird:
166−No explicit types on left hand side: Char
177+When checking left hand side of inf:
178+When checking an application of constructor Main.MkInfer:
179+ Attempting concrete match on polymorphic argument: 0
180+reg054.idr:34:1-18:
167181 |
16818234 | weird {x = Char} y = '5'
169183 | ~~~~~~~~~~~~~~~~~~
170−reg054.idr:37:1-30:When checking left hand side of weird':
171−No explicit types on left hand side: Nat
184+When checking left hand side of weird:
185+No explicit types on left hand side: Char
186+reg054.idr:37:1-30:
172187 |
17318837 | weird' {x = Prelude.Nat.Nat} y = Z
174189 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
175−reg054.idr:40:1-7:When checking left hand side of tctrick:
190+When checking left hand side of weird':
191+No explicit types on left hand side: Nat
192+reg054.idr:40:1-7:
193+ |
194+40 | tctrick (Just x) = x
195+ | ~~~~~~~
196+When checking left hand side of tctrick:
176197When checking an application of Main.tctrick:
177198 Type mismatch between
178199 Maybe a1 (Type of Just x)
179200 and
180201 a (Expected type)
181− |
182−40 | tctrick (Just x) = x
183− | ~~~~~~~
184−reg055.idr:5:1-7:When checking left hand side of g:
185−Can't match on g (f 0)
202+reg055.idr:5:1-7:
186203 |
1872045 | g (f Z) = 1
188205 | ~~~~~~~
189−reg055.idr:8:1-5:When checking left hand side of h:
190−Can't match on h x x
206+When checking left hand side of g:
207+Can't match on g (f 0)
208+reg055.idr:8:1-5:
191209 |
1922108 | h x x = x
193211 | ~~~~~
194−reg055a.idr:8:1-18:When checking left hand side of foo:
195−When checking an application of constructor Foo.CAny:
196− Attempting concrete match on polymorphic argument: Nothing
212+When checking left hand side of h:
213+Can't match on h x x
214+reg055a.idr:8:1-18:
197215 |
1982168 | foo (CAny Nothing) = 42
199217 | ~~~~~~~~~~~~~~~~~~
200−reg055a.idr:13:1-23:When checking left hand side of Foo.apply:
201−Can't match on apply (\x, y => x) a
218+When checking left hand side of foo:
219+When checking an application of constructor Foo.CAny:
220+ Attempting concrete match on polymorphic argument: Nothing
221+reg055a.idr:13:1-23:
202222 |
20322313 | apply (\x => \y => x) a = a
204224 | ~~~~~~~~~~~~~~~~~~~~~~~
205−reg056.idr:7:16-25:dodgy n m Refl is a valid case
225+When checking left hand side of Foo.apply:
226+Can't match on apply (\x, y => x) a
227+reg056.idr:7:16-25:
206228 |
2072297 | dodgy n m Refl impossible
208230 | ~~~~~~~~~~
209−reg056.idr:10:11-20:nonk Refl is a valid case
231+dodgy n m Refl is a valid case
232+reg056.idr:10:11-20:
210233 |
21123410 | nonk Refl impossible
212235 | ~~~~~~~~~~
213−reg068.idr:1:6-8:Main.nat has a name which may be implicitly bound.
214−This is likely to lead to problems!
236+nonk Refl is a valid case
237+reg068.idr:1:6-8:
215238 |
2162391 | data nat : Type where --error
217240 | ~~~
218−reg068.idr:2:8-10:Main.ze has a name which may be implicitly bound.
241+Main.nat has a name which may be implicitly bound.
219242This is likely to lead to problems!
243+reg068.idr:2:8-10:
220244 |
2212452 | ze : nat --hello.idr:10:6:When checking constructor Main.ze: !!V 0!! is not Main.nat
222246 | ~~~
247+Main.ze has a name which may be implicitly bound.
248+This is likely to lead to problems!
223249reg068.idr:2:8-10:
224−nat is bound as an implicit
225− Did you mean to refer to Main.nat?
226250 |
2272512 | ze : nat --hello.idr:10:6:When checking constructor Main.ze: !!V 0!! is not Main.nat
228252 | ~~~
229−reg068.idr:2:8-10:When checking constructor Main.ze:
230−Type level variable nat is not Main.nat
253+nat is bound as an implicit
254+ Did you mean to refer to Main.nat?
255+reg068.idr:2:8-10:
231256 |
2322572 | ze : nat --hello.idr:10:6:When checking constructor Main.ze: !!V 0!! is not Main.nat
233258 | ~~~
234−Mod.idr:11:1-22:public export Mod.natexp can't refer to export Mod.natfn
259+When checking constructor Main.ze:
260+Type level variable nat is not Main.nat
261+Mod.idr:11:1-22:
235262 |
23626311 | natexp k = S (natfn k)
237264 | ~~~~~~~~~~~~~~~~~~~~~~
265+public export Mod.natexp can't refer to export Mod.natfn
238266reg070.idr:7:1-7:
239−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
240267 |
2412687 | Show Te where
242269 | ~~~~~~~
270+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
243271./reg076.idr:8:1:
244272 |
2452738 | <empty line>
@@ -253,6 +281,9 @@ Missing fixity declaration for Main.:>
253281Missing fixity declaration for Main.:>>
254282
255283DoubleEquality.idr:4:83-103:
284+ |
285+4 | oops = the ((False = True) -> Void) (\Refl impossible) $ cong {f = (>0) . (1/)} $ the (-0.0 = 0.0) Refl
286+ | ~~~~~~~~~~~~~~~~~~~~~
256287When checking right hand side of oops with expected type
257288 Void
258289
@@ -267,14 +298,13 @@ When checking argument value to function Prelude.Basics.the:
267298 -0.0
268299 and
269300 0.0
270− |
271−4 | oops = the ((False = True) -> Void) (\Refl impossible) $ cong {f = (>0) . (1/)} $ the (-0.0 = 0.0) Refl
272− | ~~~~~~~~~~~~~~~~~~~~~
273−Canonicity.idr:9:1-9:Canonicity.f is not total as there are missing cases
301+Canonicity.idr:9:1-9:
274302 |
2753039 | f Nil = 0
276304 | ~~~~~~~~~
277−Canonicity.idr:12:1-20:Canonicity.NaN is possibly not total due to: Canonicity.f
305+Canonicity.f is not total as there are missing cases
306+Canonicity.idr:12:1-20:
278307 |
27930812 | NaN = f (Cons 0 Nil)
280309 | ~~~~~~~~~~~~~~~~~~~~
310+Canonicity.NaN is possibly not total due to: Canonicity.f
test/sourceLocation001/expected+4−4
@@ -1,23 +1,23 @@
11SourceLoc.idr:12:19-25:
2−This style of tactic proof is deprecated. See %runElab for the replacement.
32 |
4312 | getLoc : {default tactics { sourceLocation } x : SourceLocation} -> SourceLocation
54 | ~~~~~~~
6−SourceLoc.idr:21:19-23:
75This style of tactic proof is deprecated. See %runElab for the replacement.
6+SourceLoc.idr:21:19-23:
87 |
9821 | fromProofScript = proof sourceLocation
109 | ~~~~~
11−SourceLoc.idr:41:20-26:
1210This style of tactic proof is deprecated. See %runElab for the replacement.
11+SourceLoc.idr:41:20-26:
1312 |
141341 | Die : {default tactics { sourceLocation } loc : SourceLocation} -> Tm ctxt t
1514 | ~~~~~~~
16−SourceLoc.idr:99:18-22:
1715This style of tactic proof is deprecated. See %runElab for the replacement.
16+SourceLoc.idr:99:18-22:
1817 |
191899 | SourceLoc.meta = proof
2019 | ~~~~~
20+This style of tactic proof is deprecated. See %runElab for the replacement.
2121Testing using definition
2222FileLoc "SourceLoc.idr" (17, 11) (17, 16)
2323Testing using inline tactics
test/syntax001/expected+8−6
@@ -1,4 +1,8 @@
1−Syntax.idr:6:7-18:When checking right hand side of foo with expected type
1+Syntax.idr:6:7-18:
2+ |
3+6 | foo = fnord "argh"
4+ | ~~~~~~~~~~~~
5+When checking right hand side of foo with expected type
26 Nat
37
48When checking an application of function Prelude.Interfaces.+:
@@ -6,10 +10,11 @@ When checking an application of function Prelude.Interfaces.+:
610 String (Type of "argh")
711 and
812 Nat (Expected type)
13+SyntaxTest.idr:5:7-18:
914 |
10−6 | foo = fnord "argh"
15+5 | foo = fnord "argh"
1116 | ~~~~~~~~~~~~
12−SyntaxTest.idr:5:7-18:When checking right hand side of foo with expected type
17+When checking right hand side of foo with expected type
1318 Nat
1419
1520When checking an application of function Prelude.Interfaces.+:
@@ -17,6 +22,3 @@ When checking an application of function Prelude.Interfaces.+:
1722 String (Type of "argh")
1823 and
1924 Nat (Expected type)
20− |
21−5 | foo = fnord "argh"
22− | ~~~~~~~~~~~~
test/totality001/expected+6−3
@@ -1,12 +1,15 @@
1−test010.idr:15:1-30:Main.foo is possibly not total due to: Main.MkBad
1+test010.idr:15:1-30:
22 |
3315 | foo (MkBad f i) = f (MkBad' i)
44 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
5−test010a.idr:9:1-23:main.bar is possibly not total due to: main.MkBad
5+Main.foo is possibly not total due to: Main.MkBad
6+test010a.idr:9:1-23:
67 |
789 | bar = MkBad (\x => 3) 3
89 | ~~~~~~~~~~~~~~~~~~~~~~~
9−test010b.idr:9:1-23:main.bar is possibly not total due to: main.MkBad
10+main.bar is possibly not total due to: main.MkBad
11+test010b.idr:9:1-23:
1012 |
11139 | bar = MkBad (\x => 3) 3
1214 | ~~~~~~~~~~~~~~~~~~~~~~~
15+main.bar is possibly not total due to: main.MkBad
test/totality002/expected+4−3
@@ -1,14 +1,15 @@
11test017.idr:94:26-30:
2−This style of tactic proof is deprecated. See %runElab for the replacement.
32 |
4394 | maxCommutativeStepCase = proof {
54 | ~~~~~
5+This style of tactic proof is deprecated. See %runElab for the replacement.
66test017a.idr:7:1-24:
7−scg.vtrans is possibly not total due to recursive path scg.vtrans --> scg.vtrans
87 |
987 | vtrans [] _ = []
109 | ~~~~~~~~~~~~~~~~~~~~~~~~
11−test017b.idr:4:1-9:foo.foo is possibly not total due to recursive path foo.foo
10+scg.vtrans is possibly not total due to recursive path scg.vtrans --> scg.vtrans
11+test017b.idr:4:1-9:
1212 |
13134 | foo = foo
1414 | ~~~~~~~~~
15+foo.foo is possibly not total due to recursive path foo.foo
test/totality003/expected+1−1
@@ -1,5 +1,5 @@
11totality003a.idr:5:1-13:
2−smaller.qsort is possibly not total due to recursive path smaller.qsort --> smaller.qsort --> smaller.qsort
32 |
435 | qsort [] = []
54 | ~~~~~~~~~~~~~
5+smaller.qsort is possibly not total due to recursive path smaller.qsort --> smaller.qsort --> smaller.qsort
test/totality004/expected+3−2
@@ -1,10 +1,11 @@
11[1, 2, 2, 4, 3, 6, 4, 8, 5, 10]
22totality004a.idr:13:1-44:
3−Main.process is possibly not total due to recursive path Main.process --> Main.process --> Main.process
43 |
5413 | process (Get f) (x :: xs) = process (f x) xs
65 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
7−totality004a.idr:24:1-60:Main.main is possibly not total due to: Main.process
6+Main.process is possibly not total due to recursive path Main.process --> Main.process --> Main.process
7+totality004a.idr:24:1-60:
88 |
9924 | main = printLn (take 10 (process doubleInt (countStream 1)))
1010 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
11+Main.main is possibly not total due to: Main.process
test/totality006/expected+5−3
@@ -1,13 +1,15 @@
1−totality006.idr:8:1-29:Main.prf is not total as there are missing cases
1+totality006.idr:8:1-29:
22 |
338 | prf Z Z Oh impossible
44 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
5−totality006a.idr:11:21-30:prf' (S _) (S _) Oh is a valid case
5+Main.prf is not total as there are missing cases
6+totality006a.idr:11:21-30:
67 |
7811 | prf' (S _) (S _) Oh impossible
89 | ~~~~~~~~~~
10+prf' (S _) (S _) Oh is a valid case
911totality006b.idr:10:1-34:
10−totality006b.blargh is not total as there are missing cases
1112 |
121310 | blargh [] (y :: xs) so = absurd so
1314 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
15+totality006b.blargh is not total as there are missing cases
test/totality007/expected+1−1
@@ -1,8 +1,8 @@
11Entering directory `./src'
22Totality.idr:4:1-9:
3−Totality.foo is not total as there are missing cases
43 |
544 | foo Z = Z
65 | ~~~~~~~~~
6+Totality.foo is not total as there are missing cases
77Totality.idr:4:1-9:Could not build: Totality.foo is not total as there are missing cases
88Leaving directory `./src'
test/totality008/expected+2−1
@@ -1,4 +1,5 @@
1−totality008.idr:7:1-14:Main.ElimT is possibly not total due to: Main.C2
1+totality008.idr:7:1-14:
22 |
337 | ElimT _ C1 = 3
44 | ~~~~~~~~~~~~~~
5+Main.ElimT is possibly not total due to: Main.C2
test/totality009/expected+20−10
@@ -1,40 +1,50 @@
1−TestLambdaPossible.idr:9:25-34:Warning - TestLambdaPossible.case block in wrongPossible at TestLambdaPossible.idr:9:25-34 is not total as there are missing cases
1+TestLambdaPossible.idr:9:25-34:
22 |
339 | wrongPossible = (\Flase impossible)
44 | ~~~~~~~~~~
5−TestLambdaPossible.idr:9:1-35:Warning - TestLambdaPossible.wrongPossible is possibly not total due to: TestLambdaPossible.case block in wrongPossible at TestLambdaPossible.idr:9:25-34
5+Warning - TestLambdaPossible.case block in wrongPossible at TestLambdaPossible.idr:9:25-34 is not total as there are missing cases
6+TestLambdaPossible.idr:9:1-35:
67 |
789 | wrongPossible = (\Flase impossible)
89 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
9−TestLambdaPossible.idr:12:25:Warning - TestLambdaPossible.case block in wrongPossible' at TestLambdaPossible.idr:12:25 is not total as there are missing cases
10+Warning - TestLambdaPossible.wrongPossible is possibly not total due to: TestLambdaPossible.case block in wrongPossible at TestLambdaPossible.idr:9:25-34
11+TestLambdaPossible.idr:12:25:
1012 |
111312 | wrongPossible' x = case x of
1214 | ^
13−TestLambdaPossible.idr:12:1-13:40:Warning - TestLambdaPossible.wrongPossible' is possibly not total due to: TestLambdaPossible.case block in wrongPossible' at TestLambdaPossible.idr:12:25
15+Warning - TestLambdaPossible.case block in wrongPossible' at TestLambdaPossible.idr:12:25 is not total as there are missing cases
16+TestLambdaPossible.idr:12:1-13:40:
1417 |
151812 | wrongPossible' x = case x of
1619 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...
17−TestLambdaPossible.idr:9:15-35:Warning - TestLambdaPossible.case block in wrongPossible at TestLambdaPossible.idr:9:25-34 is not total as there are missing cases
20+Warning - TestLambdaPossible.wrongPossible' is possibly not total due to: TestLambdaPossible.case block in wrongPossible' at TestLambdaPossible.idr:12:25
21+TestLambdaPossible.idr:9:15-35:
1822 |
19239 | wrongPossible = (\Flase impossible)
2024 | ~~~~~~~~~~~~~~~~~~~~~
21−TestLambdaPossible.idr:9:1-35:Warning - TestLambdaPossible.wrongPossible is possibly not total due to: TestLambdaPossible.case block in wrongPossible at TestLambdaPossible.idr:9:25-34
25+Warning - TestLambdaPossible.case block in wrongPossible at TestLambdaPossible.idr:9:25-34 is not total as there are missing cases
26+TestLambdaPossible.idr:9:1-35:
2227 |
23289 | wrongPossible = (\Flase impossible)
2429 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
25−TestLambdaPossible.idr:12:18-13:40:Warning - TestLambdaPossible.case block in wrongPossible' at TestLambdaPossible.idr:12:25 is not total as there are missing cases
30+Warning - TestLambdaPossible.wrongPossible is possibly not total due to: TestLambdaPossible.case block in wrongPossible at TestLambdaPossible.idr:9:25-34
31+TestLambdaPossible.idr:12:18-13:40:
2632 |
273312 | wrongPossible' x = case x of
2834 | ~~~~~~~~~~~ ...
29−TestLambdaPossible.idr:12:1-13:40:Warning - TestLambdaPossible.wrongPossible' is possibly not total due to: TestLambdaPossible.case block in wrongPossible' at TestLambdaPossible.idr:12:25
35+Warning - TestLambdaPossible.case block in wrongPossible' at TestLambdaPossible.idr:12:25 is not total as there are missing cases
36+TestLambdaPossible.idr:12:1-13:40:
3037 |
313812 | wrongPossible' x = case x of
3239 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...
33−TestLambdaPossible2.idr:10:1-35:TestLambdaPossible.wrongPossible is possibly not total due to: TestLambdaPossible.case block in wrongPossible at TestLambdaPossible2.idr:10:25-34
40+Warning - TestLambdaPossible.wrongPossible' is possibly not total due to: TestLambdaPossible.case block in wrongPossible' at TestLambdaPossible.idr:12:25
41+TestLambdaPossible2.idr:10:1-35:
3442 |
354310 | wrongPossible = (\Flase impossible)
3644 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
37−TestLambdaPossible2.idr:14:1-15:40:TestLambdaPossible.wrongPossible' is possibly not total due to: TestLambdaPossible.case block in wrongPossible' at TestLambdaPossible2.idr:14:25
45+TestLambdaPossible.wrongPossible is possibly not total due to: TestLambdaPossible.case block in wrongPossible at TestLambdaPossible2.idr:10:25-34
46+TestLambdaPossible2.idr:14:1-15:40:
3847 |
394814 | wrongPossible' x = case x of
4049 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...
50+TestLambdaPossible.wrongPossible' is possibly not total due to: TestLambdaPossible.case block in wrongPossible' at TestLambdaPossible2.idr:14:25
test/totality010/expected+4−2
@@ -1,8 +1,10 @@
1−totality010.idr:27:1-35:Main.evenNotS is not total as there are missing cases
1+totality010.idr:27:1-35:
22 |
3327 | evenNotS MkEven ZeroEven impossible
44 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
5−totality010.idr:30:1-40:Main.bad is possibly not total due to: Main.evenNotS
5+Main.evenNotS is not total as there are missing cases
6+totality010.idr:30:1-40:
67 |
7830 | bad = evenNotS ZeroEven $ MkBad ZeroEven
89 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
10+Main.bad is possibly not total due to: Main.evenNotS
test/totality011/expected+1−1
@@ -1,5 +1,5 @@
11totality011.lidr:22:3-57:
2−Main.weCanOnlyGetOlder is not total as there are missing cases
32 |
4322 | > weCanOnlyGetOlder {t'' = Z} {t = Z} _ _ _ = LTEZero
54 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
5+Main.weCanOnlyGetOlder is not total as there are missing cases
test/totality012/expected+2−2
@@ -1,10 +1,10 @@
11totality012a.idr:9:1-10:27:
2−Main.echo2 is possibly not total due to recursive path Main.echo2 --> Main.echo2
32 |
439 | echo2 x = if (x == "quit") then PutStr "Bye!\n"
54 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...
5+Main.echo2 is possibly not total due to recursive path Main.echo2 --> Main.echo2
66totality012b.idr:11:1-17:33:
7−Main.echo is possibly not total due to recursive path Main.echo
87 |
9811 | echo = do PutStr "$ "
109 | ~~~~~~~~~~~~~~~~~~~~~ ...
10+Main.echo is possibly not total due to recursive path Main.echo
test/totality013/expected+3−2
@@ -1,9 +1,10 @@
11totality013a.idr:5:3-49:
2−Main.foo is possibly not total due to recursive path Main.foo --> Main.mtot --> Main.mtot --> Main.mtot
32 |
435 | foo order x xs y ys _ = mtot order (x :: xs) ys
54 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
6−totality013a.idr:9:3-36:Main.mtot is possibly not total due to: Main.foo
5+Main.foo is possibly not total due to recursive path Main.foo --> Main.mtot --> Main.mtot --> Main.mtot
6+totality013a.idr:9:3-36:
77 |
889 | mtot order [] right = right
99 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
10+Main.mtot is possibly not total due to: Main.foo
test/totality014/expected+5−4
@@ -1,4 +1,8 @@
1−totality014.idr:1:6-9:Universe inconsistency.
1+totality014.idr:1:6-9:
2+ |
3+1 | data Con2 : Type where
4+ | ~~~~
5+Universe inconsistency.
26 Working on: ./totality014.idr.w
37 Old domain: (5,5)
48 New domain: (5,4)
@@ -6,6 +10,3 @@ totality014.idr:1:6-9:Universe inconsistency.
610 ConstraintFC {uconstraint = ./totality014.idr.w < ./totality014.idr.u, ufc = totality014.idr:1:6-9}
711 ConstraintFC {uconstraint = ./totality014.idr.w < ./totality014.idr.u, ufc = totality014.idr:1:6-9}
812 ConstraintFC {uconstraint = ./totality014.idr.u <= ./totality014.idr.w, ufc = totality014.idr:6:27-29}
9− |
10−1 | data Con2 : Type where
11− | ~~~~
test/totality015/expected+5−3
@@ -1,13 +1,15 @@
11totality015a.idr:52:3-53:
2−Main.quiz is possibly not total due to recursive path Main.quiz --> Main.quiz
32 |
4352 | quiz (num1 :: num2 :: nums) score = quiz nums score
54 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
6−totality015a.idr:42:3-44:36:Main.correct is possibly not total due to: Main.quiz
5+Main.quiz is possibly not total due to recursive path Main.quiz --> Main.quiz
6+totality015a.idr:42:3-44:36:
77 |
8842 | correct nums score
99 | ~~~~~~~~~~~~~~~~~~ ...
10−totality015a.idr:47:3-49:28:Main.wrong is possibly not total due to: Main.quiz
10+Main.correct is possibly not total due to: Main.quiz
11+totality015a.idr:47:3-49:28:
1112 |
121347 | wrong nums ans score
1314 | ~~~~~~~~~~~~~~~~~~~~ ...
15+Main.wrong is possibly not total due to: Main.quiz
test/totality016/expected+18−9
@@ -1,36 +1,45 @@
1−totality016.idr:15:1-21:Main.f1 is not total as there are missing cases
1+totality016.idr:15:1-21:
22 |
3315 | f1 (MkTP T1 x) = True
44 | ~~~~~~~~~~~~~~~~~~~~~
5−totality016.idr:19:1-24:Main.f2 is not total as there are missing cases
5+Main.f1 is not total as there are missing cases
6+totality016.idr:19:1-24:
67 |
7819 | f2 (MkTP T1 x, _) = True
89 | ~~~~~~~~~~~~~~~~~~~~~~~~
9−totality016.idr:23:1-29:Main.f3 is not total as there are missing cases
10+Main.f2 is not total as there are missing cases
11+totality016.idr:23:1-29:
1012 |
111323 | f3 ((MkTP T1 x, _), _) = True
1214 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
13−totality016.idr:27:1-14:Main.g1 is not total as there are missing cases
15+Main.f3 is not total as there are missing cases
16+totality016.idr:27:1-14:
1417 |
151827 | g1 T1 x = True
1619 | ~~~~~~~~~~~~~~
17−totality016.idr:31:1-17:Main.g2 is not total as there are missing cases
20+Main.g1 is not total as there are missing cases
21+totality016.idr:31:1-17:
1822 |
192331 | g2 (T1, x) = True
2024 | ~~~~~~~~~~~~~~~~~
21−totality016.idr:35:1-16:Main.h1 is not total as there are missing cases
25+Main.g2 is not total as there are missing cases
26+totality016.idr:35:1-16:
2227 |
232835 | h1 True x = True
2429 | ~~~~~~~~~~~~~~~~
25−totality016.idr:39:1-19:Main.h2 is not total as there are missing cases
30+Main.h1 is not total as there are missing cases
31+totality016.idr:39:1-19:
2632 |
273339 | h2 (True, x) = True
2834 | ~~~~~~~~~~~~~~~~~~~
29−totality016.idr:43:1-25:Main.h3 is not total as there are missing cases
35+Main.h2 is not total as there are missing cases
36+totality016.idr:43:1-25:
3037 |
313843 | h3 (MkTP2 (T1, x)) = True
3239 | ~~~~~~~~~~~~~~~~~~~~~~~~~
33−totality016.idr:47:1-30:Main.h4 is not total as there are missing cases
40+Main.h3 is not total as there are missing cases
41+totality016.idr:47:1-30:
3442 |
354347 | h4 (MkTP2 (T1, x), _) _ = True
3644 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
45+Main.h4 is not total as there are missing cases
test/totality017/expected+12−6
@@ -1,24 +1,30 @@
1−totality017.idr:19:1-15:Main.g1 is not total as there are missing cases
1+totality017.idr:19:1-15:
22 |
3319 | g1 T1 T1 = True
44 | ~~~~~~~~~~~~~~~
5−totality017.idr:25:1-17:Main.g2 is not total as there are missing cases
5+Main.g1 is not total as there are missing cases
6+totality017.idr:25:1-17:
67 |
7825 | g2 T1' T1' = True
89 | ~~~~~~~~~~~~~~~~~
9−totality017.idr:31:1-13:Main.g3 is not total as there are missing cases
10+Main.g2 is not total as there are missing cases
11+totality017.idr:31:1-13:
1012 |
111331 | g3 T1' = True
1214 | ~~~~~~~~~~~~~
13−totality017.idr:37:1-36:Main.g4 is not total as there are missing cases
15+Main.g3 is not total as there are missing cases
16+totality017.idr:37:1-36:
1417 |
151837 | g4 (MkTTPP (MkPP 0) (MkPP 0)) = True
1619 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
17−totality017.idr:42:1-11:Main.f' is not total as there are missing cases
20+Main.g4 is not total as there are missing cases
21+totality017.idr:42:1-11:
1822 |
192342 | f' 0 = True
2024 | ~~~~~~~~~~~
21−totality017.idr:47:1-17:Main.f is not total as there are missing cases
25+Main.f' is not total as there are missing cases
26+totality017.idr:47:1-17:
2227 |
232847 | f (MkPP 0) = True
2429 | ~~~~~~~~~~~~~~~~~
30+Main.f is not total as there are missing cases
test/totality018/expected+2−1
@@ -1,4 +1,5 @@
1−totality018.idr:12:1-10:Main.bar is not total as there are missing cases
1+totality018.idr:12:1-10:
22 |
3312 | bar FZ = 0
44 | ~~~~~~~~~~
5+Main.bar is not total as there are missing cases
test/totality019/expected+4−2
@@ -1,8 +1,10 @@
1−totality019.idr:8:1-36:Main.testCov is not total as there are missing cases
1+totality019.idr:8:1-36:
22 |
338 | testCov False False = ?testCov_rhs_3
44 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
5−totality019.idr:12:1-42:Main.testCov' is not total as there are missing cases
5+Main.testCov is not total as there are missing cases
6+totality019.idr:12:1-42:
67 |
7812 | testCov' (False ** False) = ?testCov_rhs_3
89 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
10+Main.testCov' is not total as there are missing cases
test/totality020/expected+4−2
@@ -1,8 +1,10 @@
1−totality020.idr:4:14-23:bug _ _ Refl is a valid case
1+totality020.idr:4:14-23:
22 |
334 | bug _ _ Refl impossible
44 | ~~~~~~~~~~
5−totality020.idr:7:14-23:foo a b Refl is a valid case
5+bug _ _ Refl is a valid case
6+totality020.idr:7:14-23:
67 |
787 | foo a b Refl impossible
89 | ~~~~~~~~~~
10+foo a b Refl is a valid case
test/totality021/expected+5−5
@@ -1,25 +1,25 @@
11totality021.idr:8:1-67:
2−Main.sLevelNotSLevel' is possibly not total due to recursive path Main.sLevelNotSLevel' --> Main.sLevelNotSLevel'
32 |
438 | sLevelNotSLevel' (SL (Delay level)) p = sLevelNotSLevel' level Refl
54 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
5+Main.sLevelNotSLevel' is possibly not total due to recursive path Main.sLevelNotSLevel' --> Main.sLevelNotSLevel'
66totality021.idr:12:1-66:
7−Main.sLevelNotSLevel is possibly not total due to: Main.sLevelNotSLevel'
87 |
9812 | sLevelNotSLevel (SL (Delay level)) p = sLevelNotSLevel' level Refl
109 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
10+Main.sLevelNotSLevel is possibly not total due to: Main.sLevelNotSLevel'
1111totality021.idr:18:1-26:
12−Main.v is possibly not total due to: Main.sLevelNotSLevel
1312 |
141318 | v = sLevelNotSLevel l Refl
1514 | ~~~~~~~~~~~~~~~~~~~~~~~~~~
15+Main.v is possibly not total due to: Main.sLevelNotSLevel
1616totality021a.idr:9:1-37:
17−Main.noNonEmptyPointInt is not total as there are missing cases
1817 |
19189 | noNonEmptyPointInt {n} Nil impossible
2019 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
20+Main.noNonEmptyPointInt is not total as there are missing cases
2121totality021a.idr:12:1-31:
22−Main.myVoid is possibly not total due to: Main.noNonEmptyPointInt
2322 |
242312 | myVoid = noNonEmptyPointInt [2]
2524 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
25+Main.myVoid is possibly not total due to: Main.noNonEmptyPointInt
test/totality022/expected+2−1
@@ -1,4 +1,5 @@
1−totality022.idr:7:20-29:f _ [] (RSnoc _ _) is a valid case
1+totality022.idr:7:20-29:
22 |
337 | f _ [] (RSnoc _ _) impossible -- = ?wat
44 | ~~~~~~~~~~
5+f _ [] (RSnoc _ _) is a valid case
test/totality023/expected+1−1
@@ -1,5 +1,5 @@
11totality023.idr:9:1-10:27:
2−Main.run is possibly not total due to recursive path Main.run --> Main.run
32 |
439 | run (Do x f) = do r <- x
54 | ~~~~~~~~~~~~~~~~~~~~~~~~ ...
5+Main.run is possibly not total due to recursive path Main.run --> Main.run
test/tutorial002/expected+3−3
@@ -1,15 +1,15 @@
11tutorial002.idr:41:25-29:
2−This style of tactic proof is deprecated. See %runElab for the replacement.
32 |
4341 | Main.natToBin_lemma_1 = proof
54 | ~~~~~
6−tutorial002.idr:48:18-22:
75This style of tactic proof is deprecated. See %runElab for the replacement.
6+tutorial002.idr:48:18-22:
87 |
9848 | parity_lemma_1 = proof
109 | ~~~~~
11−tutorial002.idr:54:18-22:
1210This style of tactic proof is deprecated. See %runElab for the replacement.
11+tutorial002.idr:54:18-22:
1312 |
141354 | parity_lemma_2 = proof {
1514 | ~~~~~
15+This style of tactic proof is deprecated. See %runElab for the replacement.
test/tutorial004/expected+2−2
@@ -1,10 +1,10 @@
11tutorial004.idr:46:14-18:
2−This style of tactic proof is deprecated. See %runElab for the replacement.
32 |
4346 | plusredZ_S = proof {
54 | ~~~~~
6−tutorial004.idr:53:14-18:
75This style of tactic proof is deprecated. See %runElab for the replacement.
6+tutorial004.idr:53:14-18:
87 |
9853 | plusredZ_Z = proof {
109 | ~~~~~
10+This style of tactic proof is deprecated. See %runElab for the replacement.
test/tutorial006/expected+6−6
@@ -1,4 +1,7 @@
11tutorial006a.idr:5:23-24:
2+ |
3+5 | vapp (x :: xs) ys = x :: vapp xs xs -- BROKEN
4+ | ~~
25When checking right hand side of vapp with expected type
36 Vect (S len + m) a
47
@@ -13,10 +16,10 @@ When checking argument xs to constructor Data.Vect.:::
1316 plus len len
1417 and
1518 plus len m
16− |
17−5 | vapp (x :: xs) ys = x :: vapp xs xs -- BROKEN
18− | ~~
1919tutorial006b.idr:10:37-50:
20+ |
21+10 | parity (S (S (j + j))) | Even = Even {n=S j}
22+ | ~~~~~~~~~~~~~~
2023When checking right hand side of with block in Main.parity with expected type
2124 Parity (S (S (j + j)))
2225
@@ -30,6 +33,3 @@ Specifically:
3033 plus (S j) (S j)
3134 and
3235 S (S (plus j j))
33− |
34−10 | parity (S (S (j + j))) | Even = Even {n=S j}
35− | ~~~~~~~~~~~~~~
test/unique004/expected+27−18
@@ -1,56 +1,65 @@
1−unique001a.idr:35:14-43:50:Type mismatch between
2− Int -> String
3−and
4− UniqueType (Int -> String)
1+unique001a.idr:35:14-43:50:
52 |
6335 | showStuff xs = do
74 | ~~~~ ...
8−unique001a.idr:46:15-54:28:Type mismatch between
5+Type mismatch between
96 Int -> String
107and
118 UniqueType (Int -> String)
9+unique001a.idr:46:15-54:28:
1210 |
131146 | showStuff' xs = do
1412 | ~~~~ ...
15−unique001a.idr:57:15-62:33:Type mismatch between
16− UniqueType (Int -> String)
17−and
13+Type mismatch between
1814 Int -> String
15+and
16+ UniqueType (Int -> String)
17+unique001a.idr:57:15-62:33:
1918 |
201957 | showThings xs = do
2120 | ~~~~ ...
22−unique001b.idr:18:17-42:Borrowed name xs must not be used on RHS
21+Type mismatch between
22+ UniqueType (Int -> String)
23+and
24+ Int -> String
25+unique001b.idr:18:17-42:
2326 |
242718 | showU (x :: xs) = show x ++ "," ++ free xs
2528 | ~~~~~~~~~~~~~~~~~~~~~~~~~~
26−unique001c.idr:47:12-62:Unique name f is used more than once
29+Borrowed name xs must not be used on RHS
30+unique001c.idr:47:12-62:
2731 |
283247 | ndup {a} x = (\f : Int -> a => MkUPair (f 0) (f 1)) (uconst x)
2933 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
30−unique001d.idr:4:16-18:Borrowed name x must not be used on RHS
34+Unique name f is used more than once
35+unique001d.idr:4:16-18:
3136 |
32374 | steal (Read x) = x
3338 | ~~~
39+Borrowed name x must not be used on RHS
3440unique001e.idr:4:12-40:
35−Constructor Main.Nil has a UniqueType, but the data type does not
3641 |
37424 | Nil : {a : UniqueType} -> BadList a
3843 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
39−unique002.idr:17:8-20:19:Unique name xs is used more than once
44+Constructor Main.Nil has a UniqueType, but the data type does not
45+unique002.idr:17:8-20:19:
4046 |
414717 | foo xs = do -- let f = \x : Int => showU xs
4248 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...
43−unique002a.idr:17:8-20:19:Type mismatch between
44− Int -> String
45−and
46− UniqueType (Int -> String)
49+Unique name xs is used more than once
50+unique002a.idr:17:8-20:19:
4751 |
485217 | foo xs = do let f = \x : Int => showU xs
4953 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...
50−unique003.idr:20:8-24:19:Type mismatch between
54+Type mismatch between
5155 Int -> String
5256and
5357 UniqueType (Int -> String)
58+unique003.idr:20:8-24:19:
5459 |
556020 | foo xs = do let f = \x : Int => showU xs -- can't build this in unique context
5661 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ...
62+Type mismatch between
63+ Int -> String
64+and
65+ UniqueType (Int -> String)
test/universes001/expected+5−4
@@ -1,4 +1,8 @@
1−universes001.idr:7:5-21:Universe inconsistency.
1+universes001.idr:7:5-21:
2+ |
3+7 | foo = Const (Const 0)
4+ | ~~~~~~~~~~~~~~~~~
5+Universe inconsistency.
26 Working on: ./universes001.idr.x
37 Old domain: (5,5)
48 New domain: (5,4)
@@ -7,6 +11,3 @@ universes001.idr:7:5-21:Universe inconsistency.
711 ConstraintFC {uconstraint = ./universes001.idr.x < ./universes001.idr.y, ufc = universes001.idr:1:6-8}
812 ConstraintFC {uconstraint = ./universes001.idr.z < ./universes001.idr.x, ufc = universes001.idr:1:6-8}
913 ConstraintFC {uconstraint = ./universes001.idr.x <= ./universes001.idr.z, ufc = universes001.idr:7:5-21}
10− |
11−7 | foo = Const (Const 0)
12− | ~~~~~~~~~~~~~~~~~
test/universes002/expected+5−4
@@ -1,4 +1,8 @@
1−universes002.idr:45:9-48:Universe inconsistency.
1+universes002.idr:45:9-48:
2+ |
3+45 | russell = lemma (MkMPair (MkMPair R lemma) REFL)
4+ | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
5+Universe inconsistency.
26 Working on: ./universes002.idr.b1
37 Old domain: (5,5)
48 New domain: (5,4)
@@ -7,6 +11,3 @@ universes002.idr:45:9-48:Universe inconsistency.
711 ConstraintFC {uconstraint = ./universes002.idr.b1 < ./universes002.idr.c1, ufc = universes002.idr:3:6-10}
812 ConstraintFC {uconstraint = ./universes002.idr.b1 <= ./universes002.idr.e7, ufc = universes002.idr:45:9-48}
913 ConstraintFC {uconstraint = ./universes002.idr.d1 <= ./universes002.idr.b1, ufc = universes002.idr:3:6-10}
10− |
11−45 | russell = lemma (MkMPair (MkMPair R lemma) REFL)
12− | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~