law row_in_get

minebender-game@1.0.0.0 · proof_lists.bend:218

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

218law row_in_get:
219  for -A: Data
220  for +w: Nat
221  for +h: Nat
222  for +g: T.Grid(A)
223  for +y: Nat
224  for +sh: {B.shaped(A, w, h, g) == True{} : Bool}
225  for yh: {Nat.is_lt(y, h) == True{} : Bool}
226  {List.get(&2, List<&2, A>, g, y) == Some{row_of(A, g, y)} : Maybe<&2, List<&2, A>>}