Source/Packages

Compiler.Elaborator

packages/compiler/src/Compiler/Elaborator.alpha

1,138 lines65 declarations36.4 KiBSHA-256 71619035ff76

def · lines 173–200

elaborateBytesLengthArgument

Full file
173def elaborateBytesLengthArgument =
174  (lambda unrestricted result : (family ClosedNaturalElaboration) .
175    (eliminate
176      ClosedNaturalElaboration
177      (lambda unrestricted value : (family ClosedNaturalElaboration) .
178        (family ClosedNaturalElaboration))
179      result
180      (branch NaturalElaborated elaboratedNatural . unsupportedApplicationResult)
181      (branch
182        BytesElaborated
183        elaboratedBytes
184        .
185        (constructor
186          ClosedNaturalElaboration
187          NaturalElaborated
188          (closeNaturalLiteral (bytes-length elaboratedBytes))))
189      (branch ByteElaborated elaboratedByte . unsupportedApplicationResult)
190      (branch PrimitivePartial elaboratedPartial . unsupportedApplicationResult)
191      (branch
192        UnboundVariable
193        unboundSpelling
194        .
195        (constructor ClosedNaturalElaboration UnboundVariable unboundSpelling))
196      (branch
197        UnsupportedTerm
198        unsupportedCode
199        .
200        (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.