AlphaGitHub
Source/Packages

Compiler.LanguageEdition

packages/compiler/src/Compiler/LanguageEdition.alpha

112 lines16 declarations4.2 KiBSHA-256 75b20ed8bf85
Download exact fileView at revisionf5034773ad4bb52133

def · lines 29–49

decodeLanguageEdition

Full file
29def decodeLanguageEdition =
30  (lambda unrestricted name : Bytes .
31    (nat-eliminate
32      (lambda unrestricted matched : Nat . (family LanguageEditionDecodeResult))
33      (nat-eliminate
34        (lambda unrestricted matched : Nat . (family LanguageEditionDecodeResult))
35        (constructor LanguageEditionDecodeResult LanguageEditionRejected)
36        (lambda unrestricted predecessor : Nat .
37          (lambda unrestricted induction : (family LanguageEditionDecodeResult) .
38            (constructor
39              LanguageEditionDecodeResult
40              LanguageEditionDecoded
41              (constructor LanguageEdition Alpha2027))))
42        (bytes-equal name (languageEditionName (constructor LanguageEdition Alpha2027))))
43      (lambda unrestricted predecessor : Nat .
44        (lambda unrestricted induction : (family LanguageEditionDecodeResult) .
45          (constructor
46            LanguageEditionDecodeResult
47            LanguageEditionDecoded
48            (constructor LanguageEdition Alpha2026))))
49      (bytes-equal name (languageEditionName (constructor LanguageEdition Alpha2026)))))

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.