12233def inferCoreAppliedPrimitive2Application =
12234 (lambda unrestricted argument : (family CoreTerm) .
12235 (lambda unrestricted functionResult : (family CoreInferenceResult) .
12236 (lambda unrestricted argumentResult : (family CoreInferenceResult) .
12237 (lambda unrestricted primitive : (family CorePrimitive) .
12238 (lambda unrestricted effects : (family CoreTerm) .
12239 (lambda unrestricted resultType : (family CoreTerm) .
12240 (nat-eliminate
12241 (lambda unrestricted isBind : Nat . (family CoreInferenceResult))
12242 (inferCoreApplicationDefault argument functionResult argumentResult)
12243 (lambda unrestricted predecessor : Nat .
12244 (lambda unrestricted induction : (family CoreInferenceResult) .
12245 (inferCoreBindInput effects resultType functionResult argumentResult)))
12246 (corePrimitiveMatches primitive (constructor CorePrimitive CoreBind)))))))))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.