def at_set_ne.row

minebender-game@1.0.0.0 · proof_lists.bend:267

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

267def at_set_ne.row(-A: Data, +g: T.Grid(A), +x: Nat, +y: Nat, +qx: Nat, +v: A, +d: A,
268  xne: {Nat.is_eq(x, qx) == False{} : Bool}, +c: Bool,
269  ce: {Nat.is_lt(y, List.length(&2, List<&2, A>, g)) == c : Bool}) ->
270  {B.at(A, d, B.set_at(A, g, T.Pos{x, y}, v), T.Pos{qx, y}) == B.at(A, d, g, T.Pos{qx, y}) : A}:
271  match c:
272    case True{}:
273      +row = row_of(A, g, y)
274      +r2 = List.set(&2, A, row, x, v)
275      %Equal.sym(Maybe<&2, List<&2, A>>, List.get(&2, List<&2, A>, List.set(&2, List<&2, A>, g, y, r2), y),
276        Some{r2}, get_set_eq(List<&2, A>, g, y, r2, ce)) :
277        {Maybe.default(&2, A, List.get(&2, A, Maybe.default(&2, List<&2, A>, _, Nil{}), qx), d)
278          == B.at(A, d, g, T.Pos{qx, y}) : A}
279      %Equal.sym(Maybe<&2, A>, List.get(&2, A, r2, qx), List.get(&2, A, row, qx),
280        get_set_ne(A, row, x, qx, v, xne)) :
281        {Maybe.default(&2, A, _, d) == B.at(A, d, g, T.Pos{qx, y}) : A}
282      {==}
283    case False{}:
284      +r2 = List.set(&2, A, row_of(A, g, y), x, v)
285      %Equal.sym(T.Grid(A), List.set(&2, List<&2, A>, g, y, r2), g, set_out(List<&2, A>, g, y, r2, ce)) :
286        {B.at(A, d, _, T.Pos{qx, y}) == B.at(A, d, g, T.Pos{qx, y}) : A}
287      {==}