Source/Packages

Compiler.DependentCore

packages/compiler/src/Compiler/DependentCore.alpha

12,943 lines498 declarations489.0 KiBSHA-256 ef207b0de796

family · lines 128–185

CoreTerm

Full file
128family CoreTerm : Type 0
129constructor CoreUniverse
130field unrestricted coreUniverseLevel : Nat
131constructor CoreNatural
132constructor CoreNaturalLiteral
133field unrestricted coreNaturalValue : Bytes
134constructor CoreBound
135field unrestricted coreBoundIndex : Nat
136constructor CorePi
137field unrestricted corePiMultiplicity : (family CoreMultiplicity)
138recursive unrestricted corePiDomain
139recursive unrestricted corePiCodomain
140constructor CoreLambda
141field unrestricted coreLambdaMultiplicity : (family CoreMultiplicity)
142recursive unrestricted coreLambdaDomain
143recursive unrestricted coreLambdaBody
144constructor CoreLet
145field unrestricted coreLetMultiplicity : (family CoreMultiplicity)
146recursive unrestricted coreLetAnnotation
147recursive unrestricted coreLetValue
148recursive unrestricted coreLetBody
149constructor CoreApplication
150recursive unrestricted coreApplicationFunction
151recursive unrestricted coreApplicationArgument
152constructor CoreNaturalArithmetic
153field unrestricted coreArithmeticOperation : (family CoreNaturalOperation)
154recursive unrestricted coreArithmeticLeft
155recursive unrestricted coreArithmeticRight
156constructor CoreNaturalSuccessor
157recursive unrestricted coreNaturalPredecessor
158constructor CoreByte
159constructor CoreByteLiteral
160field unrestricted coreByteValue : Byte
161constructor CoreBytes
162constructor CoreBytesLiteral
163field unrestricted coreBytesValue : Bytes
164constructor CorePrimitiveTerm
165field unrestricted corePrimitive : (family CorePrimitive)
166constructor CoreTermSequenceEnd
167constructor CoreTermSequenceNext
168recursive unrestricted coreTermSequenceHead
169recursive unrestricted coreTermSequenceTail
170constructor CoreFamilyApplication
171field unrestricted coreFamilyName : Bytes
172recursive unrestricted coreFamilyArguments
173constructor CoreConstructorApplication
174field unrestricted coreConstructorFamilyName : Bytes
175field unrestricted coreConstructorName : Bytes
176recursive unrestricted coreConstructorArguments
177constructor CoreEliminatorBranch
178field unrestricted coreBranchConstructorName : Bytes
179field unrestricted coreBranchBinderCount : Nat
180recursive unrestricted coreBranchBody
181constructor CoreEliminator
182field unrestricted coreEliminatedFamilyName : Bytes
183recursive unrestricted coreEliminatorMotive
184recursive unrestricted coreEliminatorScrutinee
185recursive unrestricted coreEliminatorBranches

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.