def inv_assist.pick

minebender-game@1.0.0.0 · proof_inv.bend:635

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

635def inv_assist.pick(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +shown: T.Grid(Bool), +flags: List<&2, T.Pos>,
636  +status: T.Status, +sh: {B.shaped(Bool, w, h, shown) == True{} : Bool},
637  +won: {L.is_won(status) == G.all_safe(w, h, layout, shown) : Bool},
638  +cm: {calm(status, w, h, layout, shown) == True{} : Bool},
639  +cl: {closed(w, h, layout, shown) == True{} : Bool},
640  +st: {status == T.Playing{} : T.Status}, +r: Maybe<&2, T.Pos>, +k: Nat) ->
641  Inv(w, h, layout, G.assist.pick(r, G.Game{w, h, layout, shown, flags, status}, k)):
642  match r:
643    case Some{q}:
644      ({==}, ({==}, ({==}, (sh,
645        ({%st : {L.is_won(_) == G.all_safe(w, h, layout, shown) : Bool};
646          won : {False{} == G.all_safe(w, h, layout, shown) : Bool}},
647        ({==}, cl))))))
648    case None{}:
649      inv_assist.safe(w, h, layout, shown, flags, status, sh, won, cm, cl,
650        G.safe_cell(G.Game{w, h, layout, shown, flags, status}, k))