5063def reduceCoreGenericEliminator =
5064 (lambda unrestricted familyName : Bytes .
5065 (lambda unrestricted motive : (family CoreTerm) .
5066 (lambda unrestricted scrutinee : (family CoreTerm) .
5067 (lambda unrestricted branches : (family CoreTerm) .
5068 (eliminate
5069 CoreTerm
5070 (lambda unrestricted value : (family CoreTerm) . (family CoreTerm))
5071 scrutinee
5072 (branch
5073 CoreUniverse
5074 level
5075 .
5076 (constructor CoreTerm CoreEliminator familyName motive scrutinee branches))
5077 (branch
5078 CoreNatural
5079 .
5080 (constructor CoreTerm CoreEliminator familyName motive scrutinee branches))
5081 (branch
5082 CoreNaturalLiteral
5083 value
5084 .
5085 (constructor CoreTerm CoreEliminator familyName motive scrutinee branches))
5086 (branch
5087 CoreBound
5088 index
5089 .
5090 (constructor CoreTerm CoreEliminator familyName motive scrutinee branches))
5091 (branch
5092 CorePi
5093 multiplicity
5094 domain
5095 codomain
5096 ih_domain
5097 ih_codomain
5098 .
5099 (constructor CoreTerm CoreEliminator familyName motive scrutinee branches))
5100 (branch
5101 CoreLambda
5102 multiplicity
5103 domain
5104 body
5105 ih_domain
5106 ih_body
5107 .
5108 (constructor CoreTerm CoreEliminator familyName motive scrutinee branches))
5109 (branch
5110 CoreLet
5111 multiplicity
5112 annotation
5113 value
5114 body
5115 ih_annotation
5116 ih_value
5117 ih_body
5118 .
5119 (constructor
5120 CoreTerm
5121 CoreEliminator
5122 familyName
5123 motive
5124 (substituteCoreTop ih_value ih_body)
5125 branches))
5126 (branch
5127 CoreApplication
5128 function
5129 argument
5130 ih_function
5131 ih_argument
5132 .
5133 (constructor CoreTerm CoreEliminator familyName motive scrutinee branches))
5134 (branch
5135 CoreNaturalArithmetic
5136 operation
5137 function
5138 argument
5139 ih_function
5140 ih_argument
5141 .
5142 (constructor CoreTerm CoreEliminator familyName motive scrutinee branches))
5143 (branch
5144 CoreNaturalSuccessor
5145 predecessor
5146 ih_predecessor
5147 .
5148 (constructor CoreTerm CoreEliminator familyName motive scrutinee branches))
5149 (branch
5150 CoreByte
5151 .
5152 (constructor CoreTerm CoreEliminator familyName motive scrutinee branches))
5153 (branch
5154 CoreByteLiteral
5155 value
5156 .
5157 (constructor CoreTerm CoreEliminator familyName motive scrutinee branches))
5158 (branch
5159 CoreBytes
5160 .
5161 (constructor CoreTerm CoreEliminator familyName motive scrutinee branches))
5162 (branch
5163 CoreBytesLiteral
5164 value
5165 .
5166 (constructor CoreTerm CoreEliminator familyName motive scrutinee branches))
5167 (branch
5168 CorePrimitiveTerm
5169 primitive
5170 .
5171 (constructor CoreTerm CoreEliminator familyName motive scrutinee branches))
5172 (branch CoreTermSequenceEnd . (constructor CoreTerm CoreTermSequenceEnd))
5173 (branch
5174 CoreTermSequenceNext
5175 head
5176 tail
5177 ih_head
5178 ih_tail
5179 .
5180 (constructor CoreTerm CoreTermSequenceNext ih_head ih_tail))
5181 (branch
5182 CoreFamilyApplication
5183 constructorFamily
5184 arguments
5185 ih_arguments
5186 .
5187 (constructor CoreTerm CoreEliminator familyName motive scrutinee branches))
5188 (branch
5189 CoreConstructorApplication
5190 constructorFamily
5191 constructorName
5192 arguments
5193 ih_arguments
5194 .
5195 (nat-eliminate
5196 (lambda unrestricted familyMatches : Nat . (family CoreTerm))
5197 (constructor CoreTerm CoreEliminator familyName motive scrutinee branches)
5198 (lambda unrestricted predecessor : Nat .
5199 (lambda unrestricted induction : (family CoreTerm) .
5200 (finishCoreEliminatorReduction
5201 familyName
5202 motive
5203 scrutinee
5204 branches
5205 arguments
5206 ih_arguments
5207 (findCoreEliminatorBranch constructorName branches))))
5208 (coreBytesEqual constructorFamily familyName)))
5209 (branch
5210 CoreEliminatorBranch
5211 constructorName
5212 binderCount
5213 body
5214 ih_body
5215 .
5216 (constructor CoreTerm CoreEliminator familyName motive scrutinee branches))
5217 (branch
5218 CoreEliminator
5219 nestedFamily
5220 nestedMotive
5221 nestedScrutinee
5222 nestedBranches
5223 ih_motive
5224 ih_scrutinee
5225 ih_branches
5226 .
5227 (constructor CoreTerm CoreEliminator familyName motive scrutinee 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.