202def elaborateByteComparisonValue =
203 (lambda unrestricted operation : Nat .
204 (lambda unrestricted left : Byte .
205 (lambda unrestricted right : (family ClosedNaturalElaboration) .
206 (eliminate
207 ClosedNaturalElaboration
208 (lambda unrestricted value : (family ClosedNaturalElaboration) .
209 (family ClosedNaturalElaboration))
210 right
211 (branch NaturalElaborated elaboratedNatural . unsupportedApplicationResult)
212 (branch BytesElaborated elaboratedBytes . unsupportedApplicationResult)
213 (branch
214 ByteElaborated
215 elaboratedByte
216 .
217 (constructor
218 ClosedNaturalElaboration
219 NaturalElaborated
220 (closeNaturalLiteral
221 (nat-eliminate
222 (lambda unrestricted selectedOperation : Nat . Nat)
223 (byte-equal left elaboratedByte)
224 (lambda unrestricted predecessor : Nat .
225 (lambda unrestricted induction : Nat . (byte-less-than left elaboratedByte)))
226 operation))))
227 (branch PrimitivePartial elaboratedPartial . unsupportedApplicationResult)
228 (branch
229 UnboundVariable
230 unboundSpelling
231 .
232 (constructor ClosedNaturalElaboration UnboundVariable unboundSpelling))
233 (branch
234 UnsupportedTerm
235 unsupportedCode
236 .
237 (constructor ClosedNaturalElaboration UnsupportedTerm unsupportedCode))))))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.