11788def inspectCoreInferenceFunction =
11789 (lambda unrestricted term : (family CoreTerm) .
11790 (eliminate
11791 CoreTerm
11792 (lambda unrestricted value : (family CoreTerm) . (family CoreFunctionInspection))
11793 term
11794 (branch CoreUniverse level . (constructor CoreFunctionInspection CoreFunctionOther))
11795 (branch CoreNatural . (constructor CoreFunctionInspection CoreFunctionOther))
11796 (branch CoreNaturalLiteral value . (constructor CoreFunctionInspection CoreFunctionOther))
11797 (branch CoreBound index . (constructor CoreFunctionInspection CoreFunctionOther))
11798 (branch
11799 CorePi
11800 multiplicity
11801 domain
11802 codomain
11803 ih_domain
11804 ih_codomain
11805 .
11806 (constructor CoreFunctionInspection CoreFunctionOther))
11807 (branch
11808 CoreLambda
11809 multiplicity
11810 domain
11811 body
11812 ih_domain
11813 ih_body
11814 .
11815 (constructor CoreFunctionInspection CoreFunctionLambda body))
11816 (branch
11817 CoreLet
11818 multiplicity
11819 annotation
11820 value
11821 body
11822 ih_annotation
11823 ih_value
11824 ih_body
11825 .
11826 (constructor CoreFunctionInspection CoreFunctionOther))
11827 (branch
11828 CoreApplication
11829 function
11830 argument
11831 ih_function
11832 ih_argument
11833 .
11834 (extendCoreInferenceFunctionInspection ih_function argument))
11835 (branch
11836 CoreNaturalArithmetic
11837 operation
11838 function
11839 argument
11840 ih_function
11841 ih_argument
11842 .
11843 (constructor CoreFunctionInspection CoreFunctionOther))
11844 (branch
11845 CoreNaturalSuccessor
11846 predecessor
11847 ih_predecessor
11848 .
11849 (constructor CoreFunctionInspection CoreFunctionOther))
11850 (branch CoreByte . (constructor CoreFunctionInspection CoreFunctionOther))
11851 (branch CoreByteLiteral value . (constructor CoreFunctionInspection CoreFunctionOther))
11852 (branch CoreBytes . (constructor CoreFunctionInspection CoreFunctionOther))
11853 (branch CoreBytesLiteral value . (constructor CoreFunctionInspection CoreFunctionOther))
11854 (branch
11855 CorePrimitiveTerm
11856 primitive
11857 .
11858 (constructor CoreFunctionInspection CoreFunctionPrimitive primitive))
11859 (branch CoreTermSequenceEnd . (constructor CoreFunctionInspection CoreFunctionOther))
11860 (branch
11861 CoreTermSequenceNext
11862 head
11863 tail
11864 ih_head
11865 ih_tail
11866 .
11867 (constructor CoreFunctionInspection CoreFunctionOther))
11868 (branch
11869 CoreFamilyApplication
11870 familyName
11871 arguments
11872 ih_arguments
11873 .
11874 (constructor CoreFunctionInspection CoreFunctionOther))
11875 (branch
11876 CoreConstructorApplication
11877 familyName
11878 constructorName
11879 arguments
11880 ih_arguments
11881 .
11882 (constructor CoreFunctionInspection CoreFunctionOther))
11883 (branch
11884 CoreEliminatorBranch
11885 constructorName
11886 binderCount
11887 body
11888 ih_body
11889 .
11890 (constructor CoreFunctionInspection CoreFunctionOther))
11891 (branch
11892 CoreEliminator
11893 familyName
11894 motive
11895 scrutinee
11896 branches
11897 ih_motive
11898 ih_scrutinee
11899 ih_branches
11900 .
11901 (constructor CoreFunctionInspection CoreFunctionOther))))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.