git.iko.soy/Idris-dev
on master help sign in
Add --nowarnreach to two tests.
014f993Matus Tejiscak
test/proof003/Parity.idr+2−2
compare with master
unifiedsplit
@@ -1,8 +1,8 @@
1module Parity
1module Parity
2
2
3data Parity : Nat -> Type where
3data Parity : Nat -> Type where
4− even : Parity (n + n)
4+ even : {n : Nat} -> Parity (n + n)
5− odd : Parity (S (n + n))
5+ odd : {n : Nat} -> Parity (S (n + n))
6
6
7parity : (n:Nat) -> Parity n
7parity : (n:Nat) -> Parity n
8parity Z = even {n=Z}
8parity Z = even {n=Z}
test/records001/run+1−1
@@ -1,4 +1,4 @@
1#!/usr/bin/env bash
1#!/usr/bin/env bash
2−idris $@ test011.idr -o test011
2+idris $@ test011.idr -o test011 --nowarnreach
3./test011
3./test011
4rm -f test011 test011.ibc
4rm -f test011 test011.ibc
test/reg002/run+1−1
@@ -1,4 +1,4 @@
1#!/usr/bin/env bash
1#!/usr/bin/env bash
2−idris reg002.idr -o reg002
2+idris reg002.idr -o reg002 --nowarnreach
3./reg002
3./reg002
4rm -f reg002 *.ibc
4rm -f reg002 *.ibc