7176def applyCoreFunctionOnce :
7177 (pi unrestricted function : (family CoreTerm) .
7178 (pi unrestricted argument : (family CoreTerm) . (family CoreTerm))) =
7179 (lambda unrestricted function : (family CoreTerm) .
7180 (lambda unrestricted argument : (family CoreTerm) .
7181 (eliminate
7182 CoreTerm
7183 (lambda unrestricted value : (family CoreTerm) . (family CoreTerm))
7184 function
7185 (branch CoreUniverse level . (constructor CoreTerm CoreApplication function argument))
7186 (branch CoreNatural . (constructor CoreTerm CoreApplication function argument))
7187 (branch CoreNaturalLiteral value . (constructor CoreTerm CoreApplication function argument))
7188 (branch CoreBound index . (constructor CoreTerm CoreApplication function argument))
7189 (branch
7190 CorePi
7191 multiplicity
7192 domain
7193 codomain
7194 ih_domain
7195 ih_codomain
7196 .
7197 (constructor CoreTerm CoreApplication function argument))
7198 (branch
7199 CoreLambda
7200 multiplicity
7201 domain
7202 body
7203 ih_domain
7204 ih_body
7205 .
7206 (substituteCoreTop argument body))
7207 (branch
7208 CoreLet
7209 multiplicity
7210 annotation
7211 value
7212 body
7213 ih_annotation
7214 ih_value
7215 ih_body
7216 .
7217 (constructor CoreTerm CoreApplication (substituteCoreTop value body) argument))
7218 (branch
7219 CoreApplication
7220 nestedFunction
7221 nestedArgument
7222 ih_nestedFunction
7223 ih_nestedArgument
7224 .
7225 (constructor CoreTerm CoreApplication function argument))
7226 (branch
7227 CoreNaturalArithmetic
7228 operation
7229 nestedFunction
7230 nestedArgument
7231 ih_nestedFunction
7232 ih_nestedArgument
7233 .
7234 (constructor CoreTerm CoreApplication function argument))
7235 (branch
7236 CoreNaturalSuccessor
7237 predecessor
7238 ih_predecessor
7239 .
7240 (constructor CoreTerm CoreApplication function argument))
7241 (branch CoreByte . (constructor CoreTerm CoreApplication function argument))
7242 (branch CoreByteLiteral value . (constructor CoreTerm CoreApplication function argument))
7243 (branch CoreBytes . (constructor CoreTerm CoreApplication function argument))
7244 (branch CoreBytesLiteral value . (constructor CoreTerm CoreApplication function argument))
7245 (branch
7246 CorePrimitiveTerm
7247 primitive
7248 .
7249 (constructor CoreTerm CoreApplication function argument))
7250 (branch CoreTermSequenceEnd . (constructor CoreTerm CoreApplication function argument))
7251 (branch
7252 CoreTermSequenceNext
7253 head
7254 tail
7255 ih_head
7256 ih_tail
7257 .
7258 (constructor CoreTerm CoreApplication function argument))
7259 (branch
7260 CoreFamilyApplication
7261 familyName
7262 arguments
7263 ih_arguments
7264 .
7265 (constructor CoreTerm CoreApplication function argument))
7266 (branch
7267 CoreConstructorApplication
7268 familyName
7269 constructorName
7270 arguments
7271 ih_arguments
7272 .
7273 (constructor CoreTerm CoreApplication function argument))
7274 (branch
7275 CoreEliminatorBranch
7276 constructorName
7277 binderCount
7278 body
7279 ih_body
7280 .
7281 (constructor CoreTerm CoreApplication function argument))
7282 (branch
7283 CoreEliminator
7284 familyName
7285 motive
7286 scrutinee
7287 branches
7288 ih_motive
7289 ih_scrutinee
7290 ih_branches
7291 .
7292 (constructor CoreTerm CoreApplication function argument)))))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.