Compiler.Parser

4981def bareUniverseLevel =
4982  (lambda unrestricted term : (family Term) .
4983    (eliminate
4984      Term
4985      (lambda unrestricted value : (family Term) . (family NaturalTermResult))
4986      term
4987      (branch Variable spelling . (constructor NaturalTermResult NotNaturalTerm))
4988      (branch Universe level . (constructor NaturalTermResult NotNaturalTerm))
4989      (branch NaturalType . (constructor NaturalTermResult NotNaturalTerm))
4990      (branch NaturalZero . (constructor NaturalTermResult NotNaturalTerm))
4991      (branch NaturalLiteral value . (constructor NaturalTermResult NotNaturalTerm))
4992      (branch NaturalSuccessor predecessor ih . (constructor NaturalTermResult NotNaturalTerm))
4993      (branch
4994        Application
4995        function
4996        argument
4997        ihf
4998        iha
4999        .
5000        (constructor NaturalTermResult NotNaturalTerm))
5001      (branch
5002        NaturalArithmetic
5003        operation
5004        function
5005        argument
5006        ihf
5007        iha
5008        .
5009        (constructor NaturalTermResult NotNaturalTerm))
5010      (branch
5011        Lambda
5012        quantity
5013        binder
5014        domain
5015        body
5016        ihd
5017        ihb
5018        .
5019        (constructor NaturalTermResult NotNaturalTerm))
5020      (branch
5021        Pi
5022        quantity
5023        binder
5024        domain
5025        body
5026        ihd
5027        ihb
5028        .
5029        (constructor NaturalTermResult NotNaturalTerm))
5030      (branch BytesType . (constructor NaturalTermResult NotNaturalTerm))
5031      (branch BytesLiteral value . (constructor NaturalTermResult NotNaturalTerm))
5032      (branch ByteType . (constructor NaturalTermResult NotNaturalTerm))
5033      (branch ByteLiteral value . (constructor NaturalTermResult NotNaturalTerm))
5034      (branch TermSequenceEnd . (constructor NaturalTermResult NotNaturalTerm))
5035      (branch TermSequenceNext head tail ihh iht . (constructor NaturalTermResult NotNaturalTerm))
5036      (branch
5037        TermEliminatorBranch
5038        constructor
5039        binders
5040        body
5041        ihb
5042        ihbody
5043        .
5044        (constructor NaturalTermResult NotNaturalTerm))
5045      (branch
5046        FamilyApplication
5047        family
5048        arguments
5049        iha
5050        .
5051        (constructor NaturalTermResult NotNaturalTerm))
5052      (branch
5053        ConstructorApplication
5054        family
5055        constructor
5056        arguments
5057        iha
5058        .
5059        (constructor NaturalTermResult NotNaturalTerm))
5060      (branch
5061        Eliminator
5062        family
5063        motive
5064        scrutinee
5065        branches
5066        ihm
5067        ihs
5068        ihb
5069        .
5070        (constructor NaturalTermResult NotNaturalTerm))
5071      (branch
5072        Match
5073        family
5074        scrutinee
5075        branches
5076        ihs
5077        ihb
5078        .
5079        (constructor NaturalTermResult NotNaturalTerm))
5080      (branch
5081        MatchWith
5082        family
5083        motive
5084        scrutinee
5085        branches
5086        ihm
5087        ihs
5088        ihb
5089        .
5090        (constructor NaturalTermResult NotNaturalTerm))
5091      (branch
5092        IntegerLiteral
5093        spelling
5094        .
5095        (naturalLiteralAsTermValue (parseUnsignedNaturalLiteral spelling)))
5096      (branch
5097        RecordConstruction
5098        name
5099        origin
5100        bindings
5101        ih_bindings
5102        .
5103        (constructor NaturalTermResult NotNaturalTerm))
5104      (branch
5105        RecordAssignment
5106        name
5107        origin
5108        value
5109        ih_value
5110        .
5111        (constructor NaturalTermResult NotNaturalTerm))
5112      (branch
5113        RecordProjection
5114        name
5115        field
5116        origin
5117        value
5118        ih_value
5119        .
5120        (constructor NaturalTermResult NotNaturalTerm))
5121      (branch
5122        RecordUpdate
5123        name
5124        origin
5125        value
5126        bindings
5127        ih_value
5128        ih_bindings
5129        .
5130        (constructor NaturalTermResult NotNaturalTerm))
5131      (branch
5132        LocalLet
5133        quantity
5134        binder
5135        hasAnnotation
5136        annotation
5137        value
5138        body
5139        ih_annotation
5140        ih_value
5141        ih_body
5142        .
5143        (constructor NaturalTermResult NotNaturalTerm))
5144      (branch
5145        DoBlock
5146        effects
5147        result
5148        body
5149        ih_effects
5150        ih_result
5151        ih_body
5152        .
5153        (constructor NaturalTermResult NotNaturalTerm))
5154      (branch
5155        DoStep
5156        named
5157        quantity
5158        binder
5159        computation
5160        continuation
5161        ih_computation
5162        ih_continuation
5163        .
5164        (constructor NaturalTermResult NotNaturalTerm))
5165      (branch DoReturn value ih_value . (constructor NaturalTermResult NotNaturalTerm))))