Core.names_ok: def of bend-schema-lib@0.4.1.0
Import: import bend-schema-lib@0.4.1.0/core.bend as Core
Lines 1864-1908 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=1864&end_line=1908

import Base

# Every enum value in x is one of its names (encode_conforms' premise).
def names_ok(s: Schema, x: Meaning(s)) -> Bool:
  match s x:
    case SOpt{i} None{}:
      True{}
    case SOpt{i} Some{v}:
      names_ok(i, v)
    case SList{e} Nil{}:
      True{}
    case SList{+e} h <> t:
      Bool.and(names_ok(e, h), names_ok(SList{e}, t))
    case SField{n, fs, rest} Both{a, b}:
      Bool.and(names_ok(fs, a), names_ok(rest, b))
    case SRule{s2, tag} v:
      names_ok(s2, v)
    case SStrict{s2} v:
      names_ok(s2, v)
    case SStrLen{lo_, hi_, s2} v:
      names_ok(s2, v)
    case SListLen{lo_, hi_, s2} v:
      names_ok(s2, v)
    case SOptional{i} None{}:
      True{}
    case SOptional{i} Some{v}:
      names_ok(i, v)
    case STagged{k, n, cs, rest} Inl{a}:
      names_ok(cs, a)
    case STagged{k, n, cs, rest} Inr{b}:
      names_ok(rest, b)
    case SEnum{names} x:
      in_names(x, names)
    case SVariant{n, vs, rest} Inl{a}:
      names_ok(vs, a)
    case SVariant{n, vs, rest} Inr{b}:
      names_ok(rest, b)
    case STuple{ts, rest} Both{a, b}:
      Bool.and(names_ok(ts, a), names_ok(rest, b))
    case SJson{} value:
      True{}
    case SEither{l, r} Inl{a}:
      names_ok(l, a)
    case SEither{l, r} Inr{b}:
      names_ok(r, b)
    case _ _:
      True{}

Uses (9):
  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=Either
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=bend-schema-lib@0.4.1.0/core.bend&name=Both
  https://jend.leeeet.dev/definition.txt?path=bend-schema-lib@0.4.1.0/core.bend&name=Meaning
  https://jend.leeeet.dev/definition.txt?path=bend-schema-lib@0.4.1.0/core.bend&name=Schema
  https://jend.leeeet.dev/definition.txt?path=bend-schema-lib@0.4.1.0/core.bend&name=in_names