Data.JSONRender

106def jsonRenderEscapedByte =
107  (lambda unrestricted value : Byte .
108    (nat-eliminate
109      (lambda unrestricted quote : Nat . BytesBuilder)
110      (nat-eliminate
111        (lambda unrestricted slash : Nat . BytesBuilder)
112        (nat-eliminate
113          (lambda unrestricted backspace : Nat . BytesBuilder)
114          (nat-eliminate
115            (lambda unrestricted formFeed : Nat . BytesBuilder)
116            (nat-eliminate
117              (lambda unrestricted newline : Nat . BytesBuilder)
118              (nat-eliminate
119                (lambda unrestricted carriage : Nat . BytesBuilder)
120                (nat-eliminate
121                  (lambda unrestricted tab : Nat . BytesBuilder)
122                  (nat-eliminate
123                    (lambda unrestricted control : Nat . BytesBuilder)
124                    (bytes-builder-chunk (bytes-cons value b""))
125                    (lambda unrestricted predecessor : Nat .
126                      (lambda unrestricted induction : BytesBuilder .
127                        (jsonRenderEscapedControl value)))
128                    (byte-less-than value (byte 32)))
129                  (lambda unrestricted predecessor : Nat .
130                    (lambda unrestricted induction : BytesBuilder .
131                      (bytes-builder-chunk b"\\t")))
132                  (byte-equal value (byte 9)))
133                (lambda unrestricted predecessor : Nat .
134                  (lambda unrestricted induction : BytesBuilder .
135                    (bytes-builder-chunk b"\\r")))
136                (byte-equal value (byte 13)))
137              (lambda unrestricted predecessor : Nat .
138                (lambda unrestricted induction : BytesBuilder .
139                  (bytes-builder-chunk b"\\n")))
140              (byte-equal value (byte 10)))
141            (lambda unrestricted predecessor : Nat .
142              (lambda unrestricted induction : BytesBuilder . (bytes-builder-chunk b"\\f")))
143            (byte-equal value (byte 12)))
144          (lambda unrestricted predecessor : Nat .
145            (lambda unrestricted induction : BytesBuilder . (bytes-builder-chunk b"\\b")))
146          (byte-equal value (byte 8)))
147        (lambda unrestricted predecessor : Nat .
148          (lambda unrestricted induction : BytesBuilder . (bytes-builder-chunk b"\\\\")))
149        (byte-equal value (byte 92)))
150      (lambda unrestricted predecessor : Nat .
151        (lambda unrestricted induction : BytesBuilder . (bytes-builder-chunk b"\\\"")))
152      (byte-equal value (byte 34))))