11945def inferCoreEffectHead =
11946 (lambda unrestricted effects : (family CoreTerm) .
11947 (lambda unrestricted argumentResult : (family CoreInferenceResult) .
11948 (eliminate
11949 CoreInferenceResult
11950 (lambda unrestricted result : (family CoreInferenceResult) . (family CoreInferenceResult))
11951 argumentResult
11952 (branch
11953 CoreInferred
11954 effectType
11955 .
11956 (eliminate
11957 UniverseInspection
11958 (lambda unrestricted inspection : (family UniverseInspection) .
11959 (family CoreInferenceResult))
11960 (inspectUniverse effectType)
11961 (branch
11962 IsUniverse
11963 level
11964 .
11965 (nat-eliminate
11966 (lambda unrestricted valid : Nat . (family CoreInferenceResult))
11967 (constructor
11968 CoreInferenceResult
11969 CoreInferenceFailed
11970 (succ (succ (succ (succ (succ (succ zero)))))))
11971 (lambda unrestricted predecessor : Nat .
11972 (lambda unrestricted induction : (family CoreInferenceResult) .
11973 (constructor
11974 CoreInferenceResult
11975 CoreInferred
11976 (constructor CoreTerm CoreUniverse zero))))
11977 (coreEffectRowValid effects)))
11978 (branch
11979 NotUniverse
11980 .
11981 (constructor
11982 CoreInferenceResult
11983 CoreInferenceFailed
11984 (succ (succ (succ (succ (succ (succ zero))))))))))
11985 (branch
11986 CoreInferenceFailed
11987 code
11988 .
11989 (constructor CoreInferenceResult CoreInferenceFailed code)))))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.