7307def reduceCoreNaturalEliminate :
7308 (pi unrestricted motive : (family CoreTerm) .
7309 (pi unrestricted zeroCase : (family CoreTerm) .
7310 (pi unrestricted successorCase : (family CoreTerm) .
7311 (pi unrestricted scrutinee : (family CoreTerm) . (family CoreTerm))))) =
7312 (lambda unrestricted motive : (family CoreTerm) .
7313 (lambda unrestricted zeroCase : (family CoreTerm) .
7314 (lambda unrestricted successorCase : (family CoreTerm) .
7315 (lambda unrestricted scrutinee : (family CoreTerm) .
7316 (eliminate
7317 CoreLiteralInspection
7318 (lambda unrestricted inspection : (family CoreLiteralInspection) . (family CoreTerm))
7319 (inspectCoreLiteral scrutinee)
7320 (branch
7321 CoreNaturalInspected
7322 value
7323 .
7324 (second
7325 (Compiler.NaturalMagnitudeArithmetic/magnitudeIterate
7326 (sigma unrestricted predecessor : Bytes . (family CoreTerm))
7327 value
7328 (lambda unrestricted state : (sigma unrestricted predecessor : Bytes . (family CoreTerm)) .
7329 (pair
7330 (sigma unrestricted predecessor : Bytes . (family CoreTerm))
7331 (Compiler.NaturalMagnitudeArithmetic/magnitudeSuccessor (first state))
7332 (reduceNaturalEliminateStep successorCase (first state) (second state))))
7333 (pair
7334 (sigma unrestricted predecessor : Bytes . (family CoreTerm))
7335 b""
7336 zeroCase))))
7337 (branch
7338 CoreByteInspected
7339 value
7340 .
7341 (corePrimitiveApplication4
7342 (constructor CorePrimitive CoreNaturalEliminate)
7343 motive
7344 zeroCase
7345 successorCase
7346 scrutinee))
7347 (branch
7348 CoreBytesInspected
7349 value
7350 .
7351 (corePrimitiveApplication4
7352 (constructor CorePrimitive CoreNaturalEliminate)
7353 motive
7354 zeroCase
7355 successorCase
7356 scrutinee))
7357 (branch
7358 CoreNotLiteral
7359 .
7360 (corePrimitiveApplication4
7361 (constructor CorePrimitive CoreNaturalEliminate)
7362 motive
7363 zeroCase
7364 successorCase
7365 scrutinee)))))))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.