LAWS.zero_walk: def of minebender-game@1.0.0.0
Import: import minebender-game@1.0.0.0/LAWS.bend as LAWS
Lines 205-214 of minebender-game@1.0.0.0/LAWS.bend: https://jend.leeeet.dev/read.txt?path=minebender-game@1.0.0.0/LAWS.bend&start_line=205&end_line=214

import Base
import minebender-game@1.0.0.0/types.bend as T

# Starting at p, the path steps from cell to adjacent cell of the board,
# leaving only zeros, and ends at q. The empty path goes from p to p.
def zero_walk(path: List<&2, T.Pos>, +w: Nat, +h: Nat, +layout: T.Grid(Bool),
  +p: T.Pos, q: T.Pos) -> Bool:
  match path:
    case Nil{}:
      same(p, q)
    case +r <> t:
      zero(w, h, layout, p) && adjacent(p, r) && on_board(w, h, r)
        && zero_walk(t, w, h, layout, r, q)

Uses (10):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=adjacent
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=on_board
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=same
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=zero
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/types.bend&name=Grid
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/types.bend&name=Pos