def same_ne.go

minebender-game@1.0.0.0 · proof_grid.bend:202

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

202def same_ne.go(+p: T.Pos, +q: T.Pos, ne: {p != q : T.Pos}, b: Bool,
203  e: {B.same(p, q) == b : Bool}) -> {B.same(p, q) == False{} : Bool}:
204  match b:
205    case False{}:
206      e
207    case True{}:
208      Empty.absurd({B.same(p, q) == False{} : Bool}, ne(same_sound(p, q, e)))