12113def inferCoreBindInspection =
12114 (lambda unrestricted effects : (family CoreTerm) .
12115 (lambda unrestricted resultType : (family CoreTerm) .
12116 (lambda unrestricted inspection : (family CoreFunctionInspection) .
12117 (eliminate
12118 CoreFunctionInspection
12119 (lambda unrestricted value : (family CoreFunctionInspection) .
12120 (family CoreInferenceResult))
12121 inspection
12122 (branch CoreFunctionLambda body . coreEffectInferenceFailure)
12123 (branch CoreFunctionPrimitive primitive . coreEffectInferenceFailure)
12124 (branch CoreFunctionAppliedPrimitive primitive first . coreEffectInferenceFailure)
12125 (branch
12126 CoreFunctionAppliedPrimitive2
12127 primitive
12128 inputEffects
12129 inputType
12130 .
12131 (nat-eliminate
12132 (lambda unrestricted valid : Nat . (family CoreInferenceResult))
12133 coreEffectInferenceFailure
12134 (lambda unrestricted predecessor : Nat .
12135 (lambda unrestricted induction : (family CoreInferenceResult) .
12136 (coreInferredBindContinuation effects resultType inputType)))
12137 (coreNaturalAnd
12138 (corePrimitiveMatches primitive (constructor CorePrimitive CoreComputation))
12139 (coreNaturalAnd (coreEffectRowValid effects) (coreEffectRowValid inputEffects)))))
12140 (branch
12141 CoreFunctionAppliedPrimitive3
12142 primitive
12143 first
12144 second
12145 third
12146 .
12147 coreEffectInferenceFailure)
12148 (branch CoreFunctionOther . coreEffectInferenceFailure)))))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.