git.iko.soy/Idris-dev
on master help sign in
New test
e1e8b95Edwin Brady
test/README+1
compare with master
unifiedsplit
@@ -5,3 +5,4 @@ Tests:
5003: Literate source and string processing
5003: Literate source and string processing
6004: File operations
6004: File operations
7005: Num class resolution [regression]; span & break; ad-hoc overloading
7005: Num class resolution [regression]; span & break; ad-hoc overloading
8+006: Provisional definitions; class resolution in patterns
test/test006/expectednew file+1
@@ -0,0 +1 @@
1+[False, True, False, True, False, True]
test/test006/runnew file+4
@@ -0,0 +1,4 @@
1+#!/bin/bash
2+idris test006.idr -o test006
3+./test006
4+rm -f test006 test006.ibc
test/test006/test006.idrnew file+42
@@ -0,0 +1,42 @@
1+module main;
2+
3+data Parity : Nat -> Set where
4+ even : Parity (n + n)
5+ | odd : Parity (S (n + n));
6+
7+parity : (n:Nat) -> Parity n;
8+parity O = even {n=O};
9+parity (S O) = odd {n=O};
10+parity (S (S k)) with parity k {
11+ parity (S (S (j + j))) | even ?= even {n=S j};
12+ parity (S (S (S (j + j)))) | odd ?= odd {n=S j};
13+}
14+
15+
16+natToBin : Nat -> List Bool;
17+natToBin O = Nil;
18+natToBin k with parity k {
19+ natToBin (j + j) | even = False :: natToBin j;
20+ natToBin (S (j + j)) | odd = True :: natToBin j;
21+}
22+
23+main : IO ();
24+main = print (natToBin 42);
25+
26+---------- Proofs ----------
27+
28+main.parity_lemma_2 = proof {
29+ intro;
30+ intro;
31+ rewrite plusn_Sm j j;
32+ trivial;
33+};
34+
35+main.parity_lemma_1 = proof {
36+ intro j;
37+ intro;
38+ rewrite plusn_Sm j j;
39+ trivial;
40+};
41+
42+