def wcontains_works.go

minebender-game@1.0.0.0 · proof_flood.bend:204

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

204def wcontains_works.go(+r0: T.Pos, +t: List<&2, T.Pos>, +back: List<&2, T.Pos>, +q: T.Pos, +b: Bool,
205  e: {Bool.or(b, B.contains(t, q)) == True{} : Bool},
206  ih: {B.contains(t, q) == True{} : Bool} -> {wcontains(G.works(t, back), q) == True{} : Bool}) ->
207  {Bool.or(b, wcontains(G.works(t, back), q)) == True{} : Bool}:
208  match b:
209    case True{}:
210      {==}
211    case False{}:
212      ih(e)