ProofSolver.leaf_cell.go: def of minebender-game@1.0.0.0
Import: import minebender-game@1.0.0.0/proof_solver.bend as ProofSolver
Lines 863-875 of minebender-game@1.0.0.0/proof_solver.bend: https://jend.leeeet.dev/read.txt?path=minebender-game@1.0.0.0/proof_solver.bend&start_line=863&end_line=875

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/solver.bend as S
import minebender-game@1.0.0.0/proof_base.bend as P

def leaf_cell.go(+part: T.Grid(Maybe<&2, Bool>), +layout: T.Grid(Bool), +q: T.Pos, +m: Maybe<&2, Bool>,
  me: {S.look(part, q) == m : Maybe<&2, Bool>},
  cv: {Bool.not(S.is_none(m)) == True{} : Bool}, cm: {cmp_cell(m, B.mine(layout, q)) == True{} : Bool}) ->
  {beq(B.mine(S.fill(part), q), B.mine(layout, q)) == True{} : Bool}:
  match m:
    case None{}:
      Empty.absurd({beq(B.mine(S.fill(part), q), B.mine(layout, q)) == True{} : Bool}, P.false_ne_true(cv))
    case Some{c}:
      %Equal.sym(Bool, B.mine(S.fill(part), q), Maybe.default(&2, Bool, S.look(part, q), False{}), fill_at(part, q)) :
        {beq(_, B.mine(layout, q)) == True{} : Bool}
      %Equal.sym(Maybe<&2, Bool>, S.look(part, q), Some{c}, me) : {beq(Maybe.default(&2, Bool, _, False{}), B.mine(layout, q)) == True{} : Bool}
      %Equal.sym(Bool, B.mine(layout, q), c, beq_sound(B.mine(layout, q), c, cm)) : {beq(c, _) == True{} : Bool}
      beq_refl(c)

Uses (18):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.not
  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=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe.default
  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/proof_base.bend&name=false_ne_true
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_solver.bend&name=beq
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_solver.bend&name=beq_refl
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_solver.bend&name=beq_sound
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_solver.bend&name=cmp_cell
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_solver.bend&name=fill_at
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/solver.bend&name=fill
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/solver.bend&name=is_none
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/solver.bend&name=look
  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