ProofLists.at_set_ne.go: def of minebender-game@1.0.0.0
Import: import minebender-game@1.0.0.0/proof_lists.bend as ProofLists
Lines 289-309 of minebender-game@1.0.0.0/proof_lists.bend: https://jend.leeeet.dev/read.txt?path=minebender-game@1.0.0.0/proof_lists.bend&start_line=289&end_line=309

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/proof_base.bend as P

def at_set_ne.go(-A: Data, +g: T.Grid(A), +x: Nat, +y: Nat, +qx: Nat, +qy: Nat, +v: A, +d: A,
  ne: {B.same(T.Pos{x, y}, T.Pos{qx, qy}) == False{} : Bool}, +b: Bool,
  +be: {Nat.is_eq(y, qy) == b : Bool}) ->
  {B.at(A, d, B.set_at(A, g, T.Pos{x, y}, v), T.Pos{qx, qy}) == B.at(A, d, g, T.Pos{qx, qy}) : A}:
  match b:
    case False{}:
      %Equal.sym(Maybe<&2, List<&2, A>>,
        List.get(&2, List<&2, A>, List.set(&2, List<&2, A>, g, y, List.set(&2, A, row_of(A, g, y), x, v)), qy),
        List.get(&2, List<&2, A>, g, qy),
        get_set_ne(List<&2, A>, g, y, qy, List.set(&2, A, row_of(A, g, y), x, v), be)) :
        {Maybe.default(&2, A, List.get(&2, A, Maybe.default(&2, List<&2, A>, _, Nil{}), qx), d)
          == B.at(A, d, g, T.Pos{qx, qy}) : A}
      {==}
    case True{}:
      +yq = P.eq_sound(y, qy, be)
      %yq : {B.at(A, d, B.set_at(A, g, T.Pos{x, y}, v), T.Pos{qx, _}) == B.at(A, d, g, T.Pos{qx, _}) : A}
      at_set_ne.row(A, g, x, y, qx, v, d,
        {%P.and_true_r_id(Nat.is_eq(x, qx)) : {_ == False{} : Bool};
          %be : {Bool.and(Nat.is_eq(x, qx), _) == False{} : Bool};
          ne : {Nat.is_eq(x, qx) == False{} : Bool}},
        Nat.is_lt(y, List.length(&2, List<&2, A>, g)), {==})

Uses (22):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.get
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.length
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.set
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe.default
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/board.bend&name=at
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/board.bend&name=same
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/board.bend&name=set_at
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_base.bend&name=and_true_r_id
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_base.bend&name=eq_sound
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_lists.bend&name=at_set_ne.row
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_lists.bend&name=get_set_ne
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_lists.bend&name=row_of
  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