git.iko.soy/Idris-dev
on master help sign in
Remove reg008
1100e9bEdwin Brady
idris.cabal−3
compare with master
unifiedsplit
@@ -131,9 +131,6 @@ Extra-source-files:
131 test/reg007/run
131 test/reg007/run
132 test/reg007/*.lidr
132 test/reg007/*.lidr
133 test/reg007/expected
133 test/reg007/expected
134− test/reg008/run
135− test/reg008/*.idr
136− test/reg008/expected
137 test/reg009/run
134 test/reg009/run
138 test/reg009/*.lidr
135 test/reg009/*.lidr
139 test/reg009/expected
136 test/reg009/expected
test/reg008/expecteddeleted

No changes to the content.

test/reg008/reg008.idrdeleted−15
@@ -1,15 +0,0 @@
1−module NatCmp
2−
3−data Cmp : Nat -> Nat -> Type where
4− cmpLT : (y : _) -> Cmp x (x + S y)
5− cmpEQ : Cmp x x
6− cmpGT : (x : _) -> Cmp (y + S x) y
7−
8−total cmp : (x, y : Nat) -> Cmp x y
9−cmp Z Z = cmpEQ
10−cmp Z (S k) = cmpLT _
11−cmp (S k) Z = cmpGT _
12−cmp (S x) (S y) with (cmp x y)
13− cmp (S x) (S (x + (S k))) | cmpLT k = cmpLT k
14− cmp (S x) (S x) | cmpEQ = cmpEQ
15− cmp (S (y + (S k))) (S y) | cmpGT k = cmpGT k
test/reg008/rundeleted−3
@@ -1,3 +0,0 @@
1−#!/usr/bin/env bash
2−idris $@ reg008.idr --check
3−rm -f *.ibc