refactor: Data.Vect.range -> Data.List.allFins

This commit is contained in:
Kiana Sheibani 2024-12-09 02:27:33 -05:00
parent 3826a13244
commit 22423f6cf6
Signed by: toki
GPG key ID: 6CB106C25E86A9F7
2 changed files with 5 additions and 4 deletions

View file

@ -1,5 +1,6 @@
module Day4.Part1 module Day4.Part1
import Data.List
import Data.String import Data.String
import Data.Vect import Data.Vect
@ -59,8 +60,8 @@ checkString board str = go (unpack str)
export export
findChar : {h, w : _} -> Board h w -> Char -> List (Pos h w) findChar : {h, w : _} -> Board h w -> Char -> List (Pos h w)
findChar board c = do findChar board c = do
i <- toList $ range {len=h} i <- allFins h
j <- toList $ range {len=w} j <- allFins w
guard (index (i, j) board == c) guard (index (i, j) board == c)
pure (i, j) pure (i, j)

View file

@ -38,8 +38,8 @@ covering
loopPos : {h, w : _} -> (Pos h w, Direction) -> Map h w loopPos : {h, w : _} -> (Pos h w, Direction) -> Map h w
-> List (Pos h w) -> List (Pos h w)
loopPos g mp = do loopPos g mp = do
i <- toList $ range {len=h} i <- allFins h
j <- toList $ range {len=w} j <- allFins w
let obs = (i,j) let obs = (i,j)
guard (obs /= fst g && not (index obs mp)) -- must be empty space guard (obs /= fst g && not (index obs mp)) -- must be empty space
let cols = getCollisions g $ insertObs obs mp let cols = getCollisions g $ insertObs obs mp