Core.no_key: def of bend-schema-lib@0.4.1.0
Import: import bend-schema-lib@0.4.1.0/core.bend as Core
Lines 1741-1778 of bend-schema-lib@0.4.1.0/core.bend: https://jend.leeeet.dev/read.txt?path=bend-schema-lib@0.4.1.0/core.bend&start_line=1741&end_line=1778

import Base

# ---- the object a schema's encoding lands in ----
#
# enc writes an object as one flat chain of keys. An SField writes its name and
# its rest continues that object; an SVariant writes its name and the value
# under it is a chain of its own (REnd ends it, so it is a value and not a
# continuation). A wrapper -- a rule, a strict object, a bound, an optional --
# writes no key of its own and hands its value straight to its inner schema,
# so a key reaches the top of the object from inside any of them. A tagged
# case's schema is the same object the tag key was written into, and so is the
# rest of its chain.
#
# no_key is that, written down: k does not reach the top of the object enc
# builds for s, for any value of s. wf asks it of a tagged case's own schema,
# which is what keeps the tag key from being written twice.
def no_key(+k: String, s: Schema) -> Bool:
  match s:
    case SField{+n, fs, rest}:
      Bool.and(Bool.not(String.eq(n, k)), Bool.and(Bool.not(String.eq(k, n)), no_key(k, rest)))
    case SVariant{+n, vs, rest}:
      Bool.and(Bool.not(String.eq(n, k)), Bool.and(Bool.not(String.eq(k, n)), no_key(k, rest)))
    case SStrict{s2}:
      no_key(k, s2)
    case SRule{s2, tag}:
      no_key(k, s2)
    case SStrLen{lo, hi, s2}:
      no_key(k, s2)
    case SListLen{lo, hi, s2}:
      no_key(k, s2)
    case SOpt{i}:
      no_key(k, i)
    case SOptional{i}:
      no_key(k, i)
    case SEither{l, r}:
      Bool.and(no_key(k, l), no_key(k, r))
    case STagged{+k2, n2, cs2, rest2}:
      Bool.and(Bool.not(String.eq(k2, k)), Bool.and(Bool.not(String.eq(k, k2)), Bool.and(no_key(k, cs2), no_key(k, rest2))))
    case _:
      True{}

Uses (6):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.not
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String.eq
  https://jend.leeeet.dev/definition.txt?path=bend-schema-lib@0.4.1.0/core.bend&name=Schema