def mark_ok.pick

minebender-game@1.0.0.0 · proof_display.bend:234

import Base
import minebender-game@1.0.0.0/types.bend as T
import minebender-game@1.0.0.0/LAWS.bend as L

234def mark_ok.pick(+b: Bool, +t: T.Tile, ct: {L.is_covered(t) == False{} : Bool}) ->
235  {Maybe.default(&2, Bool, Maybe.map(&2, T.Tile, Bool, x => L.is_covered(x), Bool.pick(Maybe<&2, T.Tile>, b, Some{t}, None{})), False{})
236    == False{} : Bool}:
237  match b:
238    case True{}:
239      ct
240    case False{}:
241      {==}