AlphaGitHub
Source/Packages

Compiler.Elaborator

packages/compiler/src/Compiler/Elaborator.alpha

1,138 lines65 declarations36.4 KiBSHA-256 71619035ff76
Download exact fileView at revisionf5034773ad4bb52133

def · lines 144–171

elaborateNaturalToByteArgument

Full file
144def elaborateNaturalToByteArgument =
145  (lambda unrestricted result : (family ClosedNaturalElaboration) .
146    (eliminate
147      ClosedNaturalElaboration
148      (lambda unrestricted value : (family ClosedNaturalElaboration) .
149        (family ClosedNaturalElaboration))
150      result
151      (branch
152        NaturalElaborated
153        elaboratedNatural
154        .
155        (constructor
156          ClosedNaturalElaboration
157          ByteElaborated
158          (nat-to-byte (openClosedNatural elaboratedNatural))))
159      (branch BytesElaborated elaboratedBytes . unsupportedApplicationResult)
160      (branch ByteElaborated elaboratedByte . unsupportedApplicationResult)
161      (branch PrimitivePartial elaboratedPartial . unsupportedApplicationResult)
162      (branch
163        UnboundVariable
164        unboundSpelling
165        .
166        (constructor ClosedNaturalElaboration UnboundVariable unboundSpelling))
167      (branch
168        UnsupportedTerm
169        unsupportedCode
170        .
171        (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.