ProofLaws.mine_on.col: def of minebender-game@1.0.0.0
Import: import minebender-game@1.0.0.0/proof_laws.bend as ProofLaws
Lines 570-584 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=570&end_line=584

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.col(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +x: Nat, +y: Nat,
  +sh: {B.shaped(Bool, w, h, layout) == True{} : Bool}, yh: {Nat.is_lt(y, h) == True{} : Bool},
  m: {Maybe.default(&2, Bool, List.get(&2, Bool, PL.row_of(Bool, layout, y), x), False{}) == True{} : Bool},
  +b: Bool, be: {Nat.is_lt(x, w) == b : Bool}) -> {B.on_board(w, h, T.Pos{x, y}) == True{} : Bool}:
  match b:
    case True{}:
      %Equal.sym(Bool, Nat.is_lt(x, w), True{}, be) : {Bool.and(_, Nat.is_lt(y, h)) == True{} : Bool}
      yh
    case False{}:
      +row = PL.row_of(Bool, layout, y)
      Empty.absurd({B.on_board(w, h, T.Pos{x, y}) == True{} : Bool},
        P.false_ne_true(%P.get_out(Bool, row, x,
          %Equal.sym(Nat, List.length(&2, Bool, row), w, PL.row_in_len(Bool, w, h, layout, y, sh, yh)) :
            {Nat.is_lt(x, _) == False{} : Bool}; be) :
          {Maybe.default(&2, Bool, _, False{}) == True{} : Bool}; m))

Uses (17):
  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=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.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.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=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_lists.bend&name=row_in_len
  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