git.iko.soy/Idris-dev
on master help sign in
Consolidate reg034 into regression002
087a7c3Steven Shaw
test/reg034/expecteddeleted−4
compare with master
unifiedsplit
@@ -1,4 +0,0 @@
1−reg034.idr:6:5:When checking left hand side of bar:
2−Can't match on bar xs xs Refl
3−reg034.idr:9:5:When checking left hand side of foo:
4−Can't match on foo f x x Refl
test/reg034/rundeleted−3
@@ -1,3 +0,0 @@
1−#!/usr/bin/env bash
2−${IDRIS:-idris} $@ --nocolour --check reg034.idr
3−rm -f reg034 *.ibc
test/regression002/expected+4
@@ -47,3 +47,7 @@ reg028a.idr:17:14-19:
47This style of tactic proof is deprecated. See %runElab for the replacement.
47This style of tactic proof is deprecated. See %runElab for the replacement.
48reg028a.idr:11:1:
48reg028a.idr:11:1:
49tbad.qsort' is possibly not total due to: with block in tbad.qsort'
49tbad.qsort' is possibly not total due to: with block in tbad.qsort'
50+reg034.idr:6:5:When checking left hand side of bar:
51+Can't match on bar xs xs Refl
52+reg034.idr:9:5:When checking left hand side of foo:
53+Can't match on foo f x x Refl
test/reg034/reg034.idr → test/regression002/reg034.idrrenamed

The content is the same.

test/regression002/run+1
@@ -13,6 +13,7 @@ ${IDRIS:-idris} $@ --nobanner --nocolour --quiet <<!
13:load reg023.idr
13:load reg023.idr
14:load reg028.idr
14:load reg028.idr
15:load reg028a.idr
15:load reg028a.idr
16+:load reg034.idr
16!
17!
17
18
18rm -f *.ibc
19rm -f *.ibc