Source plans declare an inventory once. Refuse duplicate descriptor IDs and
schema revision aliases within that inventory; replay across native batches
still repeats identical declarations through the strict collector normally.
114def telemetryDrainDistinctDescriptor =
115 (lambda unrestricted line : Bytes .
116 (lambda unrestricted following : (family StdList Bytes) .
117 (eliminate
118 AosLine
119 (lambda unrestricted current : (family AosLine) . Nat)
120 (aosClassifyLine line)
121 (branch AosLineInvalid code . 0)
122 (branch
123 AosLineValid
124 record
125 .
126 (eliminate
127 StdList
128 (lambda unrestricted current : (family StdList Bytes) . Nat)
129 following
130 (branch StdListEmpty . 1)
131 (branch
132 StdListCons
133 head
134 tail
135 induction
136 .
137 (naturalAnd
138 induction
139 (eliminate
140 AosLine
141 (lambda unrestricted current : (family AosLine) . Nat)
142 (aosClassifyLine head)
143 (branch AosLineInvalid code . 0)
144 (branch
145 AosLineValid
146 other
147 .
148 (naturalAnd
149 (naturalIsZero
150 (bytes-equal
151 (aosMemberBytes b"descriptor_id" record)
152 (aosMemberBytes b"descriptor_id" other)))
153 (aosChoose
154 Nat
155 (naturalAnd
156 (bytes-equal (aosMemberBytes b"kind" record) b"schema")
157 (bytes-equal (aosMemberBytes b"kind" other) b"schema"))
158 (naturalIsZero
159 (bytes-equal
160 (aosMemberBytes b"schema_id" (aosMemberValue b"body" record))
161 (aosMemberBytes b"schema_id" (aosMemberValue b"body" other))))
162 1)))))))))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.