git.iko.soy/Idris-dev
on master help sign in
Consolidate reg028 into regression002
7f53344Steven Shaw
test/reg028/expecteddeleted−5
compare with master
unifiedsplit
@@ -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
42 Nat (Type of 0)
42 Nat (Type of 0)
43and
43and
44 f Nat (Expected type)
44 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 <<!
11:load reg018c.idr
11:load reg018c.idr
12:load reg018d.idr
12:load reg018d.idr
13:load reg023.idr
13:load reg023.idr
14+:load reg028.idr
15+:load reg028a.idr
14!
16!
15
17
16rm -f *.ibc
18rm -f *.ibc