def fresh_v

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

import Base

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