ProofLaws.mine_on.row: def of minebender-game@1.0.0.0
Import: import minebender-game@1.0.0.0/proof_laws.bend as ProofLaws
Lines 586-603 of minebender-game@1.0.0.0/proof_laws.bend: https://jend.leeeet.dev/read.txt?path=minebender-game@1.0.0.0/proof_laws.bend&start_line=586&end_line=603

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
import minebender-game@1.0.0.0/proof_lists.bend as PL

def mine_on.row(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +x: Nat, +y: Nat,
  +sh: {B.shaped(Bool, w, h, layout) == True{} : Bool},
  m: {B.mine(layout, T.Pos{x, y}) == True{} : Bool}, +b: Bool, +be: {Nat.is_lt(y, h) == b : Bool}) ->
  {B.on_board(w, h, T.Pos{x, y}) == True{} : Bool}:
  match b:
    case True{}:
      mine_on.col(w, h, layout, x, y, sh, be,
        %Equal.sym(Maybe<&2, List<&2, Bool>>, List.get(&2, List<&2, Bool>, layout, y), Some{PL.row_of(Bool, layout, y)},
          PL.row_in_get(Bool, w, h, layout, y, sh, be)) :
          {Maybe.default(&2, Bool, List.get(&2, Bool, Maybe.default(&2, List<&2, Bool>, _, Nil{}), x), False{}) == True{} : Bool};
        m, Nat.is_lt(x, w), {==})
    case False{}:
      Empty.absurd({B.on_board(w, h, T.Pos{x, y}) == True{} : Bool},
        P.false_ne_true(%P.get_out(List<&2, Bool>, layout, y,
          %Equal.sym(Nat, List.length(&2, List<&2, Bool>, layout), h, PL.shaped_len(Bool, w, h, layout, sh)) :
            {Nat.is_lt(y, _) == False{} : Bool}; be) :
          {Maybe.default(&2, Bool, List.get(&2, Bool, Maybe.default(&2, List<&2, Bool>, _, Nil{}), x), False{})
            == True{} : Bool}; m))

Uses (21):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  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=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_lt
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/board.bend&name=mine
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/board.bend&name=on_board
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/board.bend&name=shaped
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_base.bend&name=false_ne_true
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_base.bend&name=get_out
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_laws.bend&name=mine_on.col
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_lists.bend&name=row_in_get
  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/proof_lists.bend&name=shaped_len
  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