def display_hint.k

minebender-game@1.0.0.0 · proof_display.bend:357

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

357def display_hint.k(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +g: G.Game, +p: T.Pos,
358  +lost: {G.status(g) == T.Lost{T.AssistTooEarly{p}} : T.Status}, on: {L.on_board(w, h, p) == True{} : Bool},
359  c: PW.Canon(w, h, layout, g)) ->
360  {L.tile(g, p) == T.Hint{} : T.Tile}:
361  match c:
362    case (eg, facts):
363      +s = PW.shown_of(g)
364      +f = PW.flags_of(g)
365      %Equal.sym(G.Game, g, G.Game{w, h, layout, s, f, G.status(g)}, eg) :
366        {L.tile(_, p) == T.Hint{} : T.Tile}
367      %Equal.sym(T.Status, G.status(g), T.Lost{T.AssistTooEarly{p}}, lost) :
368        {L.tile(G.Game{w, h, layout, s, f, _}, p) == T.Hint{} : T.Tile}
369      display_hint_c(w, h, layout, s, f, p, on_conv(w, h, p, on))