ProofAssist.on_list: def of minebender-game@1.0.0.0
Import: import minebender-game@1.0.0.0/proof_assist.bend as ProofAssist
Lines 182-189 of minebender-game@1.0.0.0/proof_assist.bend: https://jend.leeeet.dev/read.txt?path=minebender-game@1.0.0.0/proof_assist.bend&start_line=182&end_line=189

import Base
import minebender-game@1.0.0.0/types.bend as T
import minebender-game@1.0.0.0/board.bend as B
import minebender-game@1.0.0.0/game.bend as G
import minebender-game@1.0.0.0/proof_cells.bend as PS

# Every cell the assist may look at is on the board.
def on_list(+w: Nat, +h: Nat, +shown: T.Grid(Bool), +k: Nat) ->
  {PS.allp(~PS.WH, ~PS.onb, PS.WH{w, h}, G.safe_list(w, h, shown, k)) == True{} : Bool}:
  +cs = B.cells(w, h)
  +es = G.edges(w, h, shown, cs)
  PS.allp_append(~PS.WH, ~PS.onb, PS.WH{w, h}, G.turn(es, k), List.append(&2, T.Pos, G.turn(cs, k), cs),
    on_turn(w, h, es, k, on_edges(w, h, shown, cs, PS.cells_on(w, h))),
    PS.allp_append(~PS.WH, ~PS.onb, PS.WH{w, h}, G.turn(cs, k), cs, on_turn(w, h, cs, k, PS.cells_on(w, h)), PS.cells_on(w, h)))

Uses (16):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.append
  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/board.bend&name=cells
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/game.bend&name=edges
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/game.bend&name=safe_list
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/game.bend&name=turn
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_assist.bend&name=on_edges
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_assist.bend&name=on_turn
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_cells.bend&name=WH
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_cells.bend&name=allp
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_cells.bend&name=allp_append
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_cells.bend&name=cells_on
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_cells.bend&name=onb
  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