269def elaborateNaturalLessThanValue =
270 (lambda unrestricted left : (family ClosedNatural) .
271 (lambda unrestricted right : (family ClosedNaturalElaboration) .
272 (eliminate
273 ClosedNaturalElaboration
274 (lambda unrestricted value : (family ClosedNaturalElaboration) .
275 (family ClosedNaturalElaboration))
276 right
277 (branch
278 NaturalElaborated
279 elaboratedNatural
280 .
281 (constructor
282 ClosedNaturalElaboration
283 NaturalElaborated
284 (closeNaturalLiteral
285 (nat-less-than (openClosedNatural left) (openClosedNatural elaboratedNatural)))))
286 (branch BytesElaborated elaboratedBytes . unsupportedApplicationResult)
287 (branch ByteElaborated elaboratedByte . unsupportedApplicationResult)
288 (branch PrimitivePartial elaboratedPartial . unsupportedApplicationResult)
289 (branch
290 UnboundVariable
291 unboundSpelling
292 .
293 (constructor ClosedNaturalElaboration UnboundVariable unboundSpelling))
294 (branch
295 UnsupportedTerm
296 unsupportedCode
297 .
298 (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.