def dfs_when_none

minebender-game@1.0.0.0 · proof_solver.bend:910

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

910def dfs_when_none(ok: Bool, k: Unit -> Maybe<&2, T.Grid(Bool)>, e: {S.dfs.when(ok, k) == None{} : Maybe<&2, T.Grid(Bool)>},
911  okt: {ok == True{} : Bool}) -> {k(Unit{}) == None{} : Maybe<&2, T.Grid(Bool)>}:
912  match ok:
913    case True{}:
914      e
915    case False{}:
916      Empty.absurd({k(Unit{}) == None{} : Maybe<&2, T.Grid(Bool)>}, P.false_ne_true(okt))