367def compileClosedNaturalElaboration =
368 (lambda unrestricted result : (family ClosedNaturalElaboration) .
369 (eliminate
370 ClosedNaturalElaboration
371 (lambda unrestricted value : (family ClosedNaturalElaboration) . (family CodegenResult))
372 result
373 (branch
374 NaturalElaborated
375 elaboratedNatural
376 .
377 (constructor CodegenResult CodeGenerated (lowerClosedNaturalValue elaboratedNatural)))
378 (branch BytesElaborated elaboratedBytes . (compileBytesValue elaboratedBytes))
379 (branch
380 ByteElaborated
381 elaboratedByte
382 .
383 (constructor CodegenResult CodeGenerated (lowerByteValue elaboratedByte)))
384 (branch
385 PrimitivePartial
386 elaboratedPartial
387 .
388 (constructor CodegenResult CodegenUnsupportedTerm (succ (succ (succ zero)))))
389 (branch
390 UnboundVariable
391 unboundSpelling
392 .
393 (constructor CodegenResult CodegenUnboundVariable unboundSpelling))
394 (branch
395 UnsupportedTerm
396 unsupportedCode
397 .
398 (constructor CodegenResult CodegenUnsupportedTerm 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.