781def sm86HeaderFields =
782 (lambda unrestricted opcode : Nat .
783 (lambda unrestricted guard : (family SM86HeaderGuard) .
784 (lambda unrestricted controlNatural : Nat .
785 (eliminate
786 SM86HeaderGuard
787 (lambda unrestricted current : (family SM86HeaderGuard) . (family SM86EncodedFieldList))
788 guard
789 (branch
790 SM86HeaderGuardValue
791 predicate
792 negated
793 .
794 (constructor
795 SM86EncodedFieldList
796 SM86EncodedFieldListCons
797 (constructor
798 SM86EncodedField
799 SM86EncodedFieldValue
800 zero
801 sm86EncodingNaturalTwelve
802 opcode)
803 (constructor
804 SM86EncodedFieldList
805 SM86EncodedFieldListCons
806 (constructor
807 SM86EncodedField
808 SM86EncodedFieldValue
809 sm86EncodingNaturalTwelve
810 sm86EncodingNaturalThree
811 predicate)
812 (constructor
813 SM86EncodedFieldList
814 SM86EncodedFieldListCons
815 (constructor
816 SM86EncodedField
817 SM86EncodedFieldValue
818 sm86EncodingNaturalFifteen
819 (succ zero)
820 negated)
821 (constructor
822 SM86EncodedFieldList
823 SM86EncodedFieldListCons
824 (constructor
825 SM86EncodedField
826 SM86EncodedFieldValue
827 sm86EncodingNaturalOneHundredFive
828 sm86EncodingNaturalTwentyThree
829 controlNatural)
830 (constructor SM86EncodedFieldList SM86EncodedFieldListEmpty))))))))))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.