def fresh_f

bend-schema-lib@0.4.1.0 · core.bend:1780

import Base

1780# n is not a key of the record chain s (a chain ends in SEnd). Both orders are
1781# asked, as fresh_v asks them: which of the two names a step puts first depends
1782# on which of them is the value's key there, and asking both spares a proof
1783# that String.eq is symmetric.
1784def fresh_f(+n: String, s: Schema) -> Bool:
1785  match s:
1786    case SField{+m, fs, rest}:
1787      Bool.and(Bool.not(String.eq(m, n)), Bool.and(Bool.not(String.eq(n, m)), fresh_f(n, rest)))
1788    case SEnd{}:
1789      True{}
1790    case _:
1791      False{}