11908def coreEffectRowValid =
11909 (lambda unrestricted row : (family CoreTerm) .
11910 (eliminate
11911 CoreFunctionInspection
11912 (lambda unrestricted inspection : (family CoreFunctionInspection) . Nat)
11913 (inspectCoreInferenceFunction row)
11914 (branch CoreFunctionLambda body . zero)
11915 (branch CoreFunctionPrimitive primitive . zero)
11916 (branch
11917 CoreFunctionAppliedPrimitive
11918 primitive
11919 effect
11920 .
11921 (nat-eliminate
11922 (lambda unrestricted matched : Nat . Nat)
11923 zero
11924 (lambda unrestricted predecessor : Nat .
11925 (lambda unrestricted induction : Nat .
11926 (eliminate
11927 CoreFunctionInspection
11928 (lambda unrestricted effectInspection : (family CoreFunctionInspection) . Nat)
11929 (inspectCoreInferenceFunction effect)
11930 (branch CoreFunctionLambda body . zero)
11931 (branch
11932 CoreFunctionPrimitive
11933 effectPrimitive
11934 .
11935 (corePrimitiveMatches effectPrimitive (constructor CorePrimitive CoreFileEffect)))
11936 (branch CoreFunctionAppliedPrimitive ignored first . zero)
11937 (branch CoreFunctionAppliedPrimitive2 ignored first second . zero)
11938 (branch CoreFunctionAppliedPrimitive3 ignored first second third . zero)
11939 (branch CoreFunctionOther . zero))))
11940 (corePrimitiveMatches primitive (constructor CorePrimitive CoreEffects))))
11941 (branch CoreFunctionAppliedPrimitive2 primitive first second . zero)
11942 (branch CoreFunctionAppliedPrimitive3 primitive first second third . zero)
11943 (branch CoreFunctionOther . 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.