def on_turn

minebender-game@1.0.0.0 · proof_assist.bend:145

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

145def on_turn(+w: Nat, +h: Nat, +ps: List<&2, T.Pos>, +k: Nat,
146  +on: {PS.allp(~PS.WH, ~PS.onb, PS.WH{w, h}, ps) == True{} : Bool}) ->
147  {PS.allp(~PS.WH, ~PS.onb, PS.WH{w, h}, G.turn(ps, k)) == True{} : Bool}:
148  +i = Nat.mod(k, Nat.add(List.length(&2, T.Pos, ps), 1n))
149  PS.allp_append(~PS.WH, ~PS.onb, PS.WH{w, h}, List.drop(&2, T.Pos, ps, i), List.take(&2, T.Pos, ps, i),
150    on_drop(w, h, ps, i, on), on_take(w, h, ps, i, on))