git.iko.soy/Idris-dev
on master help sign in
Fix usage in reg025.
843238dMatus Tejiscak
test/reg025/reg025.idr+1−1
compare with master
unifiedsplit
@@ -9,7 +9,7 @@ Cell n = Maybe (Fin n)
9data Board : Nat -> Type where
9data Board : Nat -> Type where
10 MkBoard : {n : Nat} -> Vect n (Vect n (Cell n)) -> Board n
10 MkBoard : {n : Nat} -> Vect n (Vect n (Cell n)) -> Board n
11
11
12−emptyBoard : Board n
12+emptyBoard : {n : Nat} -> Board n
13emptyBoard {n=n} = MkBoard (replicate n (replicate n Nothing))
13emptyBoard {n=n} = MkBoard (replicate n (replicate n Nothing))
14
14
15Empty : Cell n -> Type
15Empty : Cell n -> Type