12213def inferCoreAppliedPrimitiveApplication =
12214 (lambda unrestricted argument : (family CoreTerm) .
12215 (lambda unrestricted functionResult : (family CoreInferenceResult) .
12216 (lambda unrestricted argumentResult : (family CoreInferenceResult) .
12217 (lambda unrestricted primitive : (family CorePrimitive) .
12218 (lambda unrestricted effects : (family CoreTerm) .
12219 (nat-eliminate
12220 (lambda unrestricted isReturn : Nat . (family CoreInferenceResult))
12221 (nat-eliminate
12222 (lambda unrestricted isBind : Nat . (family CoreInferenceResult))
12223 (inferCoreApplicationDefault argument functionResult argumentResult)
12224 (lambda unrestricted predecessor : Nat .
12225 (lambda unrestricted induction : (family CoreInferenceResult) .
12226 (inferCoreBindResultType functionResult argumentResult)))
12227 (corePrimitiveMatches primitive (constructor CorePrimitive CoreBind)))
12228 (lambda unrestricted predecessor : Nat .
12229 (lambda unrestricted induction : (family CoreInferenceResult) .
12230 (inferCoreReturnApplication effects functionResult argumentResult)))
12231 (corePrimitiveMatches primitive (constructor CorePrimitive CoreReturn))))))))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.