Consolidate reg028 into regression002
commit7f53344c16cea1bdb1b4a8d9de57bd9a80f83a83
authorSteven Shaw <steven@steshaw.org>
dateFri 5 Aug 2016, 20:32 (10 years ago)
parenteac558e
test/reg028/expecteddeleted−5
@@ -1,5 +0,0 @@
1−reg028.idr:5:1:tbad.bad is possibly not total due to: with block in tbad.bad
2−reg028a.idr:17:14-19:
3−This style of tactic proof is deprecated. See %runElab for the replacement.
4−reg028a.idr:11:1:
5−tbad.qsort' is possibly not total due to: with block in tbad.qsort'
test/reg028/rundeleted−4
@@ -1,4 +0,0 @@
1−#!/usr/bin/env bash
2−${IDRIS:-idris} $@ reg028.idr --check
3−${IDRIS:-idris} $@ reg028a.idr --check
4−rm -f *.ibc
test/regression002/expected+5
@@ -42,3 +42,8 @@ Type mismatch between
4242 Nat (Type of 0)
4343and
4444 f Nat (Expected type)
45+reg028.idr:5:1:tbad.bad is possibly not total due to: with block in tbad.bad
46+reg028a.idr:17:14-19:
47+This style of tactic proof is deprecated. See %runElab for the replacement.
48+reg028a.idr:11:1:
49+tbad.qsort' is possibly not total due to: with block in tbad.qsort'
test/reg028/reg028.idr → test/regression002/reg028.idrrenamed
The content is the same.
test/reg028/reg028a.idr → test/regression002/reg028a.idrrenamed
The content is the same.
test/regression002/run+2
@@ -11,6 +11,8 @@ ${IDRIS:-idris} $@ --nobanner --nocolour --quiet <<!
1111:load reg018c.idr
1212:load reg018d.idr
1313:load reg023.idr
14+:load reg028.idr
15+:load reg028a.idr
1416!
1517
1618rm -f *.ibc