Remove reg008

Functions its testing is now part of the library
This commit is contained in:
Edwin Brady 2014-06-10 19:19:30 +01:00
parent 5ca9ef85a9
commit 1100e9b0d3
4 changed files with 0 additions and 21 deletions

View File

@ -131,9 +131,6 @@ Extra-source-files:
test/reg007/run
test/reg007/*.lidr
test/reg007/expected
test/reg008/run
test/reg008/*.idr
test/reg008/expected
test/reg009/run
test/reg009/*.lidr
test/reg009/expected

View File

View File

@ -1,15 +0,0 @@
module NatCmp
data Cmp : Nat -> Nat -> Type where
cmpLT : (y : _) -> Cmp x (x + S y)
cmpEQ : Cmp x x
cmpGT : (x : _) -> Cmp (y + S x) y
total cmp : (x, y : Nat) -> Cmp x y
cmp Z Z = cmpEQ
cmp Z (S k) = cmpLT _
cmp (S k) Z = cmpGT _
cmp (S x) (S y) with (cmp x y)
cmp (S x) (S (x + (S k))) | cmpLT k = cmpLT k
cmp (S x) (S x) | cmpEQ = cmpEQ
cmp (S (y + (S k))) (S y) | cmpGT k = cmpGT k

View File

@ -1,3 +0,0 @@
#!/usr/bin/env bash
idris $@ reg008.idr --check
rm -f *.ibc