115def elaborateByteToNaturalArgument =
116 (lambda unrestricted result : (family ClosedNaturalElaboration) .
117 (eliminate
118 ClosedNaturalElaboration
119 (lambda unrestricted value : (family ClosedNaturalElaboration) .
120 (family ClosedNaturalElaboration))
121 result
122 (branch NaturalElaborated elaboratedNatural . unsupportedApplicationResult)
123 (branch BytesElaborated elaboratedBytes . unsupportedApplicationResult)
124 (branch
125 ByteElaborated
126 elaboratedByte
127 .
128 (constructor
129 ClosedNaturalElaboration
130 NaturalElaborated
131 (closeNaturalLiteral (byte-to-nat elaboratedByte))))
132 (branch PrimitivePartial elaboratedPartial . unsupportedApplicationResult)
133 (branch
134 UnboundVariable
135 unboundSpelling
136 .
137 (constructor ClosedNaturalElaboration UnboundVariable unboundSpelling))
138 (branch
139 UnsupportedTerm
140 unsupportedCode
141 .
142 (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.