def dfs_or_none_r

minebender-game@1.0.0.0 · proof_solver.bend:926

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

926def dfs_or_none_r(r: Maybe<&2, T.Grid(Bool)>, k: Unit -> Maybe<&2, T.Grid(Bool)>,
927  e: {S.dfs.or(r, k) == None{} : Maybe<&2, T.Grid(Bool)>}) -> {k(Unit{}) == None{} : Maybe<&2, T.Grid(Bool)>}:
928  match r:
929    case None{}:
930      e
931    case Some{l}:
932      Empty.absurd({k(Unit{}) == None{} : Maybe<&2, T.Grid(Bool)>}, some_ne_none(T.Grid(Bool), l, e))