def allp_member

minebender-game@1.0.0.0 · proof_cells.bend:38

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/proof_base.bend as P

38# A cell of a list whose cells all pass f passes f.
39def allp_member(~E: Data, ~f: E -> T.Pos -> Bool, +e: E, ps: List<&2, T.Pos>, +q: T.Pos,
40  +h: {allp(~E, ~f, e, ps) == True{} : Bool}, m: {B.contains(ps, q) == True{} : Bool}) ->
41  {f(e, q) == True{} : Bool}:
42  match ps:
43    case Nil{}:
44      Empty.absurd({f(e, q) == True{} : Bool}, P.false_ne_true(m))
45    case +p <> +t:
46      allp_member.go(~E, ~f, e, p, t, q, allp_head(~E, ~f, e, p, t, h), B.same(p, q), {==}, m,
47        mt => allp_member(~E, ~f, e, t, q, allp_tail(~E, ~f, e, p, t, h), mt))