Fix usage in reg025.
commit843238de65c7e4008ed60926a2e8b25d07a9b1ce
authorMatus Tejiscak <ziman@functor.sk>
dateTue 11 Mar 2014, 12:11 (13 years ago)
parentadc7d08
test/reg025/reg025.idr+1−1
@@ -9,7 +9,7 @@ Cell n = Maybe (Fin n)
99data Board : Nat -> Type where
1010 MkBoard : {n : Nat} -> Vect n (Vect n (Cell n)) -> Board n
1111
12−emptyBoard : Board n
12+emptyBoard : {n : Nat} -> Board n
1313emptyBoard {n=n} = MkBoard (replicate n (replicate n Nothing))
1414
1515Empty : Cell n -> Type