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

import Base

# n is not a key of the variant chain s (a chain ends in SVEnd). Both orders
# are asked: reading a key compares the names one way, reading past it the
# other, and asking both spares a proof that String.eq is symmetric.
def fresh_v(+n: String, s: Schema) -> Bool:
  match s:
    case SVariant{+m, vs, rest}:
      Bool.and(Bool.not(String.eq(m, n)), Bool.and(Bool.not(String.eq(n, m)), fresh_v(n, rest)))
    case SVEnd{}:
      True{}
    case _:
      False{}

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