def dfs_when_some

minebender-game@1.0.0.0 · proof_solver.bend:1069

import Base
import minebender-game@1.0.0.0/types.bend as T
import minebender-game@1.0.0.0/solver.bend as S
import minebender-game@1.0.0.0/proof_lists.bend as PL

1069def dfs_when_some(ok: Bool, k: Unit -> Maybe<&2, T.Grid(Bool)>, -l: T.Grid(Bool),
1070  e: {S.dfs.when(ok, k) == Some{l} : Maybe<&2, T.Grid(Bool)>}) -> {k(Unit{}) == Some{l} : Maybe<&2, T.Grid(Bool)>}:
1071  match ok:
1072    case True{}:
1073      e
1074    case False{}:
1075      Empty.absurd({k(Unit{}) == Some{l} : Maybe<&2, T.Grid(Bool)>}, PL.none_ne_some(T.Grid(Bool), l, e))