def leaf_some

minebender-game@1.0.0.0 · proof_solver.bend:1104

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

1104def leaf_some(+ctx: S.Ctx, +f: T.Grid(Bool), +l: T.Grid(Bool), +b: Bool, be: {S.check(ctx, f) == b : Bool},
1105  e: {Bool.pick(Maybe<&2, T.Grid(Bool)>, b, Some{f}, None{}) == Some{l} : Maybe<&2, T.Grid(Bool)>}) ->
1106  {f == l : T.Grid(Bool)} & {S.check(ctx, f) == True{} : Bool}:
1107  match b:
1108    case True{}:
1109      (PL.some_inj(T.Grid(Bool), f, l, e), be)
1110    case False{}:
1111      Empty.absurd({f == l : T.Grid(Bool)} & {S.check(ctx, f) == True{} : Bool}, PL.none_ne_some(T.Grid(Bool), l, e))