AlphaGitHub
Source/Packages

Compiler.DependentCore

packages/compiler/src/Compiler/DependentCore.alpha

12,943 lines498 declarations489.0 KiBSHA-256 ef207b0de796
Download exact fileView at revisionf5034773ad4bb52133

def · lines 1009–1018

multiplicityCode

Full file
1009def multiplicityCode : (pi unrestricted multiplicity : (family CoreMultiplicity) . Nat) =
1010  (lambda unrestricted multiplicity : (family CoreMultiplicity) .
1011    (eliminate
1012      CoreMultiplicity
1013      (lambda unrestricted value : (family CoreMultiplicity) . Nat)
1014      multiplicity
1015      (branch CoreErased . zero)
1016      (branch CoreLinear . (succ zero))
1017      (branch CoreAffine . (succ (succ zero)))
1018      (branch CoreUnrestricted . (succ (succ (succ zero))))))

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.