Remove reg008
Functions its testing is now part of the library
commit1100e9b0d378cc690f4c4d93df7eb7ce2f74428f
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateTue 10 Jun 2014, 19:19 (12 years ago)
parent5ca9ef8
idris.cabal−3
@@ -131,9 +131,6 @@ Extra-source-files:
131131 test/reg007/run
132132 test/reg007/*.lidr
133133 test/reg007/expected
134− test/reg008/run
135− test/reg008/*.idr
136− test/reg008/expected
137134 test/reg009/run
138135 test/reg009/*.lidr
139136 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