Operand witnesses establish Nat typing. The proof predicate consumes the
same checked normal forms directly, without constructing an inference result.
12403def coreArithmeticAdmissionRight =
12404 (lambda unrestricted operation : (family CoreNaturalOperation) .
12405 (lambda unrestricted left : (family CoreTerm) .
12406 (lambda unrestricted rightResult : (family CoreReductionResult) .
12407 (eliminate
12408 CoreReductionResult
12409 (lambda unrestricted result : (family CoreReductionResult) . Nat)
12410 rightResult
12411 (branch
12412 CoreReductionCompleted
12413 right
12414 rounds
12415 .
12416 (eliminate
12417 CoreArithmeticInspection
12418 (lambda unrestricted inspection : (family CoreArithmeticInspection) . Nat)
12419 (inspectCoreArithmetic operation left right)
12420 (branch CoreArithmeticValue digits . (succ zero))
12421 (branch CoreArithmeticNeutral . (succ zero))
12422 (branch CoreArithmeticRejected failure . zero)))
12423 (branch CoreReductionExhausted residual rounds . 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.