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

import Base

# n is not a key of the record chain s (a chain ends in SEnd). Both orders are
# asked, as fresh_v asks them: which of the two names a step puts first depends
# on which of them is the value's key there, and asking both spares a proof
# that String.eq is symmetric.
def fresh_f(+n: String, s: Schema) -> Bool:
  match s:
    case SField{+m, fs, rest}:
      Bool.and(Bool.not(String.eq(m, n)), Bool.and(Bool.not(String.eq(n, m)), fresh_f(n, rest)))
    case SEnd{}:
      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