11634def inferApplicationNormalizedDomain =
11635 (lambda unrestricted budget : Nat .
11636 (lambda unrestricted argument : (family CoreTerm) .
11637 (lambda unrestricted codomain : (family CoreTerm) .
11638 (lambda unrestricted argumentType : (family CoreTerm) .
11639 (lambda unrestricted domain : (family CoreTerm) .
11640 (app
11641 (nat-eliminate
11642 (lambda unrestricted equal : Nat .
11643 (pi unrestricted trigger : Nat . (family CoreInferenceResult)))
11644 (lambda unrestricted trigger : Nat .
11645 (constructor CoreInferenceResult CoreInferenceFailed (byte-to-nat (byte 6))))
11646 (lambda unrestricted predecessor : Nat .
11647 (lambda unrestricted induction : (pi unrestricted trigger : Nat . (family CoreInferenceResult)) .
11648 (lambda unrestricted trigger : Nat .
11649 (inferNormalizedCoreTypeWithBudget
11650 budget
11651 (substituteCoreTop argument codomain)))))
11652 (coreTermEqual argumentType domain))
11653 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.