Closed successors normalize through the same literal reducer as evaluation.
2942def normalizeCoreType : (pi unrestricted term : (family CoreTerm) . (family CoreTerm)) =
2943 (lambda unrestricted term : (family CoreTerm) .
2944 (eliminate
2945 CoreTerm
2946 (lambda unrestricted value : (family CoreTerm) . (family CoreTerm))
2947 term
2948 (branch CoreUniverse level . (constructor CoreTerm CoreUniverse level))
2949 (branch CoreNatural . (constructor CoreTerm CoreNatural))
2950 (branch CoreNaturalLiteral value . (constructor CoreTerm CoreNaturalLiteral value))
2951 (branch CoreBound index . (constructor CoreTerm CoreBound index))
2952 (branch
2953 CorePi
2954 multiplicity
2955 domain
2956 codomain
2957 ih_domain
2958 ih_codomain
2959 .
2960 (constructor CoreTerm CorePi multiplicity ih_domain ih_codomain))
2961 (branch
2962 CoreLambda
2963 multiplicity
2964 domain
2965 body
2966 ih_domain
2967 ih_body
2968 .
2969 (constructor CoreTerm CoreLambda multiplicity ih_domain ih_body))
2970 (branch
2971 CoreLet
2972 multiplicity
2973 annotation
2974 value
2975 body
2976 ih_annotation
2977 ih_value
2978 ih_body
2979 .
2980 (substituteCoreTop ih_value ih_body))
2981 (branch
2982 CoreApplication
2983 function
2984 argument
2985 ih_function
2986 ih_argument
2987 .
2988 (reduceCoreTypeApplication ih_function ih_argument))
2989 (branch
2990 CoreNaturalArithmetic
2991 operation
2992 function
2993 argument
2994 ih_function
2995 ih_argument
2996 .
2997 (reduceCoreArithmetic operation ih_function ih_argument))
2998 (branch
2999 CoreNaturalSuccessor
3000 predecessor
3001 ih_predecessor
3002 .
3003 (reduceCoreNaturalSuccessor ih_predecessor))
3004 (branch CoreByte . (constructor CoreTerm CoreByte))
3005 (branch CoreByteLiteral value . (constructor CoreTerm CoreByteLiteral value))
3006 (branch CoreBytes . (constructor CoreTerm CoreBytes))
3007 (branch CoreBytesLiteral value . (constructor CoreTerm CoreBytesLiteral value))
3008 (branch CorePrimitiveTerm primitive . (constructor CoreTerm CorePrimitiveTerm primitive))
3009 (branch CoreTermSequenceEnd . (constructor CoreTerm CoreTermSequenceEnd))
3010 (branch
3011 CoreTermSequenceNext
3012 head
3013 tail
3014 ih_head
3015 ih_tail
3016 .
3017 (constructor CoreTerm CoreTermSequenceNext ih_head ih_tail))
3018 (branch
3019 CoreFamilyApplication
3020 familyName
3021 arguments
3022 ih_arguments
3023 .
3024 (constructor CoreTerm CoreFamilyApplication familyName ih_arguments))
3025 (branch
3026 CoreConstructorApplication
3027 familyName
3028 constructorName
3029 arguments
3030 ih_arguments
3031 .
3032 (constructor CoreTerm CoreConstructorApplication familyName constructorName ih_arguments))
3033 (branch
3034 CoreEliminatorBranch
3035 constructorName
3036 binderCount
3037 body
3038 ih_body
3039 .
3040 (constructor CoreTerm CoreEliminatorBranch constructorName binderCount ih_body))
3041 (branch
3042 CoreEliminator
3043 familyName
3044 motive
3045 scrutinee
3046 branches
3047 ih_motive
3048 ih_scrutinee
3049 ih_branches
3050 .
3051 (constructor CoreTerm CoreEliminator familyName ih_motive ih_scrutinee ih_branches))))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.