def dfs_or_none_l

minebender-game@1.0.0.0 · proof_solver.bend:918

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

918def dfs_or_none_l(r: Maybe<&2, T.Grid(Bool)>, k: Unit -> Maybe<&2, T.Grid(Bool)>,
919  e: {S.dfs.or(r, k) == None{} : Maybe<&2, T.Grid(Bool)>}) -> {r == None{} : Maybe<&2, T.Grid(Bool)>}:
920  match r:
921    case None{}:
922      {==}
923    case Some{l}:
924      Empty.absurd({Some{l} == None{} : Maybe<&2, T.Grid(Bool)>}, some_ne_none(T.Grid(Bool), l, e))