git.iko.soy/Idris-dev
on master help sign in
Add reg003 tests
718a040Edwin Brady
test/reg003/expectednew file+4
compare with master
unifiedsplit
@@ -0,0 +1,4 @@
1+reg003a.idr:4:No such variable OddList
2+reg003a.idr:7:No such variable EvenList
3+reg003a.idr:10:No such variable EvenList
4+reg003a.idr:10:No type declaration for test
test/reg003/reg003.idrnew file+13
@@ -0,0 +1,13 @@
1+
2+mutual
3+ namespace Even
4+ data EvenList : Set where
5+ Nil : EvenList
6+ (::) : Nat -> OddList -> EvenList
7+
8+ namespace Odd
9+ data OddList : Set where
10+ (::) : Nat -> EvenList -> OddList
11+
12+test : EvenList
13+test = [1, 2, 3, 4, 5, 6]
test/reg003/reg003a.idrnew file+10
@@ -0,0 +1,10 @@
1+
2+data EvenList : Set where
3+ ENil : EvenList
4+ ECons : Nat -> OddList -> EvenList
5+
6+data OddList : Set where
7+ OCons : Nat -> EvenList -> OddList
8+
9+test : EvenList
10+test = ECons 1 ENil
test/reg003/runnew file+4
@@ -0,0 +1,4 @@
1+#!/bin/bash
2+idris --check reg003.idr
3+idris --check reg003a.idr
4+rm -f *.ibc