11366def inspectPi : (pi unrestricted term : (family CoreTerm) . (family PiInspection)) =
11367 (lambda unrestricted term : (family CoreTerm) .
11368 (eliminate
11369 CoreTerm
11370 (lambda unrestricted value : (family CoreTerm) . (family PiInspection))
11371 term
11372 (branch CoreUniverse level . (constructor PiInspection NotPi))
11373 (branch CoreNatural . (constructor PiInspection NotPi))
11374 (branch CoreNaturalLiteral value . (constructor PiInspection NotPi))
11375 (branch CoreBound index . (constructor PiInspection NotPi))
11376 (branch
11377 CorePi
11378 multiplicity
11379 domain
11380 codomain
11381 ih_domain
11382 ih_codomain
11383 .
11384 (constructor PiInspection IsPi multiplicity domain codomain))
11385 (branch
11386 CoreLambda
11387 multiplicity
11388 domain
11389 body
11390 ih_domain
11391 ih_body
11392 .
11393 (constructor PiInspection NotPi))
11394 (branch
11395 CoreLet
11396 multiplicity
11397 annotation
11398 value
11399 body
11400 ih_annotation
11401 ih_value
11402 ih_body
11403 .
11404 (constructor PiInspection NotPi))
11405 (branch
11406 CoreApplication
11407 function
11408 argument
11409 ih_function
11410 ih_argument
11411 .
11412 (constructor PiInspection NotPi))
11413 (branch
11414 CoreNaturalArithmetic
11415 operation
11416 function
11417 argument
11418 ih_function
11419 ih_argument
11420 .
11421 (constructor PiInspection NotPi))
11422 (branch CoreNaturalSuccessor predecessor ih_predecessor . (constructor PiInspection NotPi))
11423 (branch CoreByte . (constructor PiInspection NotPi))
11424 (branch CoreByteLiteral value . (constructor PiInspection NotPi))
11425 (branch CoreBytes . (constructor PiInspection NotPi))
11426 (branch CoreBytesLiteral value . (constructor PiInspection NotPi))
11427 (branch CorePrimitiveTerm primitive . (constructor PiInspection NotPi))
11428 (branch CoreTermSequenceEnd . (constructor PiInspection NotPi))
11429 (branch CoreTermSequenceNext head tail ih_head ih_tail . (constructor PiInspection NotPi))
11430 (branch
11431 CoreFamilyApplication
11432 familyName
11433 arguments
11434 ih_arguments
11435 .
11436 (constructor PiInspection NotPi))
11437 (branch
11438 CoreConstructorApplication
11439 familyName
11440 constructorName
11441 arguments
11442 ih_arguments
11443 .
11444 (constructor PiInspection NotPi))
11445 (branch
11446 CoreEliminatorBranch
11447 constructorName
11448 binderCount
11449 body
11450 ih_body
11451 .
11452 (constructor PiInspection NotPi))
11453 (branch
11454 CoreEliminator
11455 familyName
11456 motive
11457 scrutinee
11458 branches
11459 ih_motive
11460 ih_scrutinee
11461 ih_branches
11462 .
11463 (constructor PiInspection NotPi))))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.