4357def decodeNullaryTerm =
4358 (lambda unrestricted term : (family Term) .
4359 (eliminate
4360 Term
4361 (lambda unrestricted value : (family Term) . (family TermDecodeResult))
4362 term
4363 (branch
4364 Variable
4365 spelling
4366 .
4367 (eliminate
4368 NaturalOperationLookup
4369 (lambda unrestricted result : (family NaturalOperationLookup) . (family TermDecodeResult))
4370 (Compiler.NaturalOperation/lookupNaturalOperation spelling)
4371 (branch NaturalOperationFound operation . arithmeticArityFailure)
4372 (branch
4373 NaturalOperationMissing
4374 .
4375 (chooseNamedDecode
4376 (bytesEqual spelling bytesLiteralSpelling)
4377 (lambda unrestricted force : Nat .
4378 (constructor TermDecodeResult TermDecoded (constructor Term BytesLiteral b"")))
4379 (lambda unrestricted force : Nat . (constructor TermDecodeResult TermDecoded term))))))
4380 (branch Universe level . (constructor TermDecodeResult TermDecoded term))
4381 (branch NaturalType . (constructor TermDecodeResult TermDecoded term))
4382 (branch NaturalZero . (constructor TermDecodeResult TermDecoded term))
4383 (branch NaturalLiteral naturalLiteralValue . (constructor TermDecodeResult TermDecoded term))
4384 (branch
4385 NaturalSuccessor
4386 predecessor
4387 ih_predecessor
4388 .
4389 (constructor TermDecodeResult TermDecoded term))
4390 (branch
4391 Application
4392 function
4393 argument
4394 ih_function
4395 ih_argument
4396 .
4397 (constructor TermDecodeResult TermDecoded term))
4398 (branch
4399 NaturalArithmetic
4400 operation
4401 function
4402 argument
4403 ih_function
4404 ih_argument
4405 .
4406 (constructor TermDecodeResult TermDecoded term))
4407 (branch
4408 Lambda
4409 quantityTag
4410 binderSpelling
4411 domain
4412 body
4413 ih_domain
4414 ih_body
4415 .
4416 (constructor TermDecodeResult TermDecoded term))
4417 (branch
4418 Pi
4419 quantityTag
4420 binderSpelling
4421 domain
4422 codomain
4423 ih_domain
4424 ih_codomain
4425 .
4426 (constructor TermDecodeResult TermDecoded term))
4427 (branch BytesType . (constructor TermDecodeResult TermDecoded term))
4428 (branch BytesLiteral bytesValue . (constructor TermDecodeResult TermDecoded term))
4429 (branch ByteType . (constructor TermDecodeResult TermDecoded term))
4430 (branch ByteLiteral byteValue . (constructor TermDecodeResult TermDecoded term))
4431 (branch TermSequenceEnd . (constructor TermDecodeResult TermDecoded term))
4432 (branch
4433 TermSequenceNext
4434 sequenceHead
4435 sequenceTail
4436 ih_sequenceHead
4437 ih_sequenceTail
4438 .
4439 (constructor TermDecodeResult TermDecoded term))
4440 (branch
4441 TermEliminatorBranch
4442 constructorSpelling
4443 binderNames
4444 body
4445 ih_binderNames
4446 ih_body
4447 .
4448 (constructor TermDecodeResult TermDecoded term))
4449 (branch
4450 FamilyApplication
4451 familySpelling
4452 familyArguments
4453 ih_familyArguments
4454 .
4455 (constructor TermDecodeResult TermDecoded term))
4456 (branch
4457 ConstructorApplication
4458 familySpelling
4459 constructorSpelling
4460 constructorArguments
4461 ih_constructorArguments
4462 .
4463 (constructor TermDecodeResult TermDecoded term))
4464 (branch
4465 Eliminator
4466 eliminatedFamilySpelling
4467 motive
4468 scrutinee
4469 branches
4470 ih_motive
4471 ih_scrutinee
4472 ih_branches
4473 .
4474 (constructor TermDecodeResult TermDecoded term))
4475 (branch
4476 Match
4477 family
4478 scrutinee
4479 branches
4480 ih_scrutinee
4481 ih_branches
4482 .
4483 (constructor TermDecodeResult TermDecoded term))
4484 (branch
4485 MatchWith
4486 family
4487 motive
4488 scrutinee
4489 branches
4490 ih_motive
4491 ih_scrutinee
4492 ih_branches
4493 .
4494 (constructor TermDecodeResult TermDecoded term))
4495 (branch
4496 IntegerLiteral
4497 integerLiteralSpelling
4498 .
4499 (constructor TermDecodeResult TermDecoded term))
4500 (branch
4501 RecordConstruction
4502 name
4503 origin
4504 bindings
4505 ih_bindings
4506 .
4507 (constructor TermDecodeResult TermDecoded term))
4508 (branch
4509 RecordAssignment
4510 name
4511 origin
4512 value
4513 ih_value
4514 .
4515 (constructor TermDecodeResult TermDecoded term))
4516 (branch
4517 RecordProjection
4518 name
4519 field
4520 origin
4521 value
4522 ih_value
4523 .
4524 (constructor TermDecodeResult TermDecoded term))
4525 (branch
4526 RecordUpdate
4527 name
4528 origin
4529 value
4530 bindings
4531 ih_value
4532 ih_bindings
4533 .
4534 (constructor TermDecodeResult TermDecoded term))
4535 (branch
4536 LocalLet
4537 quantity
4538 binder
4539 hasAnnotation
4540 annotation
4541 value
4542 body
4543 ih_annotation
4544 ih_value
4545 ih_body
4546 .
4547 (constructor TermDecodeResult TermDecoded term))
4548 (branch
4549 DoBlock
4550 effects
4551 result
4552 body
4553 ih_effects
4554 ih_result
4555 ih_body
4556 .
4557 (constructor TermDecodeResult TermDecoded term))
4558 (branch
4559 DoStep
4560 named
4561 quantity
4562 binder
4563 computation
4564 continuation
4565 ih_computation
4566 ih_continuation
4567 .
4568 (constructor TermDecodeResult TermDecoded term))
4569 (branch DoReturn value ih_value . (constructor TermDecodeResult TermDecoded term))))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.