5328def inspectCoreFunction :
5329 (pi unrestricted term : (family CoreTerm) . (family CoreFunctionInspection)) =
5330 (lambda unrestricted term : (family CoreTerm) .
5331 (eliminate
5332 CoreTerm
5333 (lambda unrestricted value : (family CoreTerm) . (family CoreFunctionInspection))
5334 term
5335 (branch CoreUniverse level . (constructor CoreFunctionInspection CoreFunctionOther))
5336 (branch CoreNatural . (constructor CoreFunctionInspection CoreFunctionOther))
5337 (branch CoreNaturalLiteral value . (constructor CoreFunctionInspection CoreFunctionOther))
5338 (branch CoreBound index . (constructor CoreFunctionInspection CoreFunctionOther))
5339 (branch
5340 CorePi
5341 multiplicity
5342 domain
5343 codomain
5344 ih_domain
5345 ih_codomain
5346 .
5347 (constructor CoreFunctionInspection CoreFunctionOther))
5348 (branch
5349 CoreLambda
5350 multiplicity
5351 domain
5352 body
5353 ih_domain
5354 ih_body
5355 .
5356 (constructor CoreFunctionInspection CoreFunctionLambda body))
5357 (branch
5358 CoreLet
5359 multiplicity
5360 annotation
5361 value
5362 body
5363 ih_annotation
5364 ih_value
5365 ih_body
5366 .
5367 (constructor CoreFunctionInspection CoreFunctionOther))
5368 (branch
5369 CoreApplication
5370 function
5371 argument
5372 ih_function
5373 ih_argument
5374 .
5375 (extendCoreFunctionInspection ih_function argument))
5376 (branch
5377 CoreNaturalArithmetic
5378 operation
5379 function
5380 argument
5381 ih_function
5382 ih_argument
5383 .
5384 (constructor CoreFunctionInspection CoreFunctionOther))
5385 (branch
5386 CoreNaturalSuccessor
5387 predecessor
5388 ih_predecessor
5389 .
5390 (constructor CoreFunctionInspection CoreFunctionOther))
5391 (branch CoreByte . (constructor CoreFunctionInspection CoreFunctionOther))
5392 (branch CoreByteLiteral value . (constructor CoreFunctionInspection CoreFunctionOther))
5393 (branch CoreBytes . (constructor CoreFunctionInspection CoreFunctionOther))
5394 (branch CoreBytesLiteral value . (constructor CoreFunctionInspection CoreFunctionOther))
5395 (branch
5396 CorePrimitiveTerm
5397 primitive
5398 .
5399 (constructor CoreFunctionInspection CoreFunctionPrimitive primitive))
5400 (branch CoreTermSequenceEnd . (constructor CoreFunctionInspection CoreFunctionOther))
5401 (branch
5402 CoreTermSequenceNext
5403 head
5404 tail
5405 ih_head
5406 ih_tail
5407 .
5408 (constructor CoreFunctionInspection CoreFunctionOther))
5409 (branch
5410 CoreFamilyApplication
5411 familyName
5412 arguments
5413 ih_arguments
5414 .
5415 (constructor CoreFunctionInspection CoreFunctionOther))
5416 (branch
5417 CoreConstructorApplication
5418 familyName
5419 constructorName
5420 arguments
5421 ih_arguments
5422 .
5423 (constructor CoreFunctionInspection CoreFunctionOther))
5424 (branch
5425 CoreEliminatorBranch
5426 constructorName
5427 binderCount
5428 body
5429 ih_body
5430 .
5431 (constructor CoreFunctionInspection CoreFunctionOther))
5432 (branch
5433 CoreEliminator
5434 familyName
5435 motive
5436 scrutinee
5437 branches
5438 ih_motive
5439 ih_scrutinee
5440 ih_branches
5441 .
5442 (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.