law know_rows_get

minebender-game@1.0.0.0 · proof_grid.bend:60

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

60law know_rows_get:
61  for +w: Nat
62  for +h: Nat
63  for +layout: T.Grid(Bool)
64  for +shown: T.Grid(Bool)
65  for +ys: List<&2, Nat>
66  for +i: Nat
67  for +y: Nat
68  for e: {List.get(&2, Nat, ys, i) == Some{y} : Maybe<&2, Nat>}
69  {List.get(&2, List<&2, T.Seen>, G.know_rows(w, h, layout, shown, ys), i)
70    == Some{G.know_row(w, h, layout, shown, y, List.range(w))} : Maybe<&2, List<&2, T.Seen>>}