Fix usage in basic002.
commitc181edbd669b9ad94bbf4fc0de1f000179901fc3
authorMatus Tejiscak <ziman@functor.sk>
dateThu 27 Feb 2014, 11:42 (13 years ago)
parentbfd9900
test/basic002/test006.idr+2−2
@@ -1,8 +1,8 @@
11module Main
22
33data Parity : Nat -> Type where
4− even : Parity (n + n)
5− odd : Parity (S (n + n))
4+ even : {n : Nat} -> Parity (n + n)
5+ odd : {n : Nat} -> Parity (S (n + n))
66
77parity : (n:Nat) -> Parity n
88parity Z = even {n=Z}