12502def finishInferCoreLetValue =
12503 (lambda unrestricted annotation : (family CoreTerm) .
12504 (lambda unrestricted value : (family CoreTerm) .
12505 (lambda unrestricted valueResult : (family CoreInferenceResult) .
12506 (lambda unrestricted bodyResult : (family CoreInferenceResult) .
12507 (eliminate
12508 CoreInferenceResult
12509 (lambda unrestricted result : (family CoreInferenceResult) .
12510 (family CoreInferenceResult))
12511 valueResult
12512 (branch
12513 CoreInferred
12514 valueType
12515 .
12516 (nat-eliminate
12517 (lambda unrestricted matches : Nat . (family CoreInferenceResult))
12518 (constructor
12519 CoreInferenceResult
12520 CoreInferenceFailed
12521 (succ (succ (succ (succ (succ zero))))))
12522 (lambda unrestricted predecessor : Nat .
12523 (lambda unrestricted induction : (family CoreInferenceResult) .
12524 (finishInferCoreLetBody value bodyResult)))
12525 (coreTermEqual (normalizeCoreType valueType) (normalizeCoreType annotation))))
12526 (branch
12527 CoreInferenceFailed
12528 code
12529 .
12530 (constructor CoreInferenceResult CoreInferenceFailed code)))))))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.