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 43–51

closeNaturalLiteral

Full file
43def closeNaturalLiteral =
44  (lambda unrestricted value : Nat .
45    (nat-eliminate
46      (lambda unrestricted remaining : Nat . (family ClosedNatural))
47      (constructor ClosedNatural ClosedZero)
48      (lambda unrestricted predecessor : Nat .
49        (lambda unrestricted induction : (family ClosedNatural) .
50          (constructor ClosedNatural ClosedSuccessor induction)))
51      value))

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.