719def jsonBoolean =
720 (lambda unrestricted value : (family JSON) .
721 (eliminate
722 JSON
723 (lambda unrestricted current : (family JSON) . (family JSONBooleanAccessResult))
724 value
725 (branch
726 JSONObject
727 members
728 membersInduction
729 .
730 (constructor
731 JSONBooleanAccessResult
732 JSONBooleanAccessFailed
733 (constructor JSONErrorCode JSONExpectedBoolean)))
734 (branch
735 JSONObjectEnd
736 .
737 (constructor
738 JSONBooleanAccessResult
739 JSONBooleanAccessFailed
740 (constructor JSONErrorCode JSONExpectedBoolean)))
741 (branch
742 JSONObjectMember
743 key
744 member
745 tail
746 memberInduction
747 tailInduction
748 .
749 (constructor
750 JSONBooleanAccessResult
751 JSONBooleanAccessFailed
752 (constructor JSONErrorCode JSONExpectedBoolean)))
753 (branch
754 JSONArray
755 values
756 valuesInduction
757 .
758 (constructor
759 JSONBooleanAccessResult
760 JSONBooleanAccessFailed
761 (constructor JSONErrorCode JSONExpectedBoolean)))
762 (branch
763 JSONArrayEnd
764 .
765 (constructor
766 JSONBooleanAccessResult
767 JSONBooleanAccessFailed
768 (constructor JSONErrorCode JSONExpectedBoolean)))
769 (branch
770 JSONArrayNext
771 head
772 tail
773 headInduction
774 tailInduction
775 .
776 (constructor
777 JSONBooleanAccessResult
778 JSONBooleanAccessFailed
779 (constructor JSONErrorCode JSONExpectedBoolean)))
780 (branch
781 JSONString
782 text
783 .
784 (constructor
785 JSONBooleanAccessResult
786 JSONBooleanAccessFailed
787 (constructor JSONErrorCode JSONExpectedBoolean)))
788 (branch
789 JSONNumber
790 number
791 .
792 (constructor
793 JSONBooleanAccessResult
794 JSONBooleanAccessFailed
795 (constructor JSONErrorCode JSONExpectedBoolean)))
796 (branch
797 JSONBoolean
798 boolean
799 .
800 (nat-eliminate
801 (lambda unrestricted valid : Nat . (family JSONBooleanAccessResult))
802 (constructor
803 JSONBooleanAccessResult
804 JSONBooleanAccessFailed
805 (constructor JSONErrorCode JSONMalformedTree))
806 (lambda unrestricted predecessor : Nat .
807 (lambda unrestricted induction : (family JSONBooleanAccessResult) .
808 (constructor JSONBooleanAccessResult JSONBooleanAccessSucceeded boolean)))
809 (nat-less-than boolean jsonNaturalTwo)))
810 (branch
811 JSONNull
812 .
813 (constructor
814 JSONBooleanAccessResult
815 JSONBooleanAccessFailed
816 (constructor JSONErrorCode JSONExpectedBoolean)))))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.