Source/Packages

Compiler.Elaborator

packages/compiler/src/Compiler/Elaborator.alpha

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

def · lines 86–113

elaborateSuccessorArgument

Full file
86def elaborateSuccessorArgument =
87  (lambda unrestricted result : (family ClosedNaturalElaboration) .
88    (eliminate
89      ClosedNaturalElaboration
90      (lambda unrestricted value : (family ClosedNaturalElaboration) .
91        (family ClosedNaturalElaboration))
92      result
93      (branch
94        NaturalElaborated
95        elaboratedNatural
96        .
97        (constructor
98          ClosedNaturalElaboration
99          NaturalElaborated
100          (constructor ClosedNatural ClosedSuccessor elaboratedNatural)))
101      (branch BytesElaborated elaboratedBytes . unsupportedApplicationResult)
102      (branch ByteElaborated elaboratedByte . unsupportedApplicationResult)
103      (branch PrimitivePartial elaboratedPartial . unsupportedApplicationResult)
104      (branch
105        UnboundVariable
106        unboundSpelling
107        .
108        (constructor ClosedNaturalElaboration UnboundVariable unboundSpelling))
109      (branch
110        UnsupportedTerm
111        unsupportedCode
112        .
113        (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.