Compiler.DependentCore

11255def inspectUniverse : (pi unrestricted term : (family CoreTerm) . (family UniverseInspection)) =
11256  (lambda unrestricted term : (family CoreTerm) .
11257    (eliminate
11258      CoreTerm
11259      (lambda unrestricted value : (family CoreTerm) . (family UniverseInspection))
11260      term
11261      (branch CoreUniverse level . (constructor UniverseInspection IsUniverse level))
11262      (branch CoreNatural . (constructor UniverseInspection NotUniverse))
11263      (branch CoreNaturalLiteral value . (constructor UniverseInspection NotUniverse))
11264      (branch CoreBound index . (constructor UniverseInspection NotUniverse))
11265      (branch
11266        CorePi
11267        multiplicity
11268        domain
11269        codomain
11270        ih_domain
11271        ih_codomain
11272        .
11273        (constructor UniverseInspection NotUniverse))
11274      (branch
11275        CoreLambda
11276        multiplicity
11277        domain
11278        body
11279        ih_domain
11280        ih_body
11281        .
11282        (constructor UniverseInspection NotUniverse))
11283      (branch
11284        CoreLet
11285        multiplicity
11286        annotation
11287        value
11288        body
11289        ih_annotation
11290        ih_value
11291        ih_body
11292        .
11293        (constructor UniverseInspection NotUniverse))
11294      (branch
11295        CoreApplication
11296        function
11297        argument
11298        ih_function
11299        ih_argument
11300        .
11301        (constructor UniverseInspection NotUniverse))
11302      (branch
11303        CoreNaturalArithmetic
11304        operation
11305        function
11306        argument
11307        ih_function
11308        ih_argument
11309        .
11310        (constructor UniverseInspection NotUniverse))
11311      (branch
11312        CoreNaturalSuccessor
11313        predecessor
11314        ih_predecessor
11315        .
11316        (constructor UniverseInspection NotUniverse))
11317      (branch CoreByte . (constructor UniverseInspection NotUniverse))
11318      (branch CoreByteLiteral value . (constructor UniverseInspection NotUniverse))
11319      (branch CoreBytes . (constructor UniverseInspection NotUniverse))
11320      (branch CoreBytesLiteral value . (constructor UniverseInspection NotUniverse))
11321      (branch CorePrimitiveTerm primitive . (constructor UniverseInspection NotUniverse))
11322      (branch CoreTermSequenceEnd . (constructor UniverseInspection NotUniverse))
11323      (branch
11324        CoreTermSequenceNext
11325        head
11326        tail
11327        ih_head
11328        ih_tail
11329        .
11330        (constructor UniverseInspection NotUniverse))
11331      (branch
11332        CoreFamilyApplication
11333        familyName
11334        arguments
11335        ih_arguments
11336        .
11337        (constructor UniverseInspection NotUniverse))
11338      (branch
11339        CoreConstructorApplication
11340        familyName
11341        constructorName
11342        arguments
11343        ih_arguments
11344        .
11345        (constructor UniverseInspection NotUniverse))
11346      (branch
11347        CoreEliminatorBranch
11348        constructorName
11349        binderCount
11350        body
11351        ih_body
11352        .
11353        (constructor UniverseInspection NotUniverse))
11354      (branch
11355        CoreEliminator
11356        familyName
11357        motive
11358        scrutinee
11359        branches
11360        ih_motive
11361        ih_scrutinee
11362        ih_branches
11363        .
11364        (constructor UniverseInspection NotUniverse))))