proof/JSON_SourceProof.bend checks

raw source on the hub · import qasim-bend-kit@0.1.0.2/proof/JSON_SourceProof.bend as JSON_SourceProof

9 imports

import Base
import ../libs/JSON.bend as J
import ./JSON_AssemblyProof.bend as A
import ./JSON_PrimitiveProof.bend as P
import ./JSON_StringProof.bend as S
import ./JSON_ParallelProof.bend as Par
import ./JSON_NumberLexProof.bend as Num
import ./JSON_LexWhitespaceProof.bend as W
import ./JSON_ListProof.bend as LP

Types

type AtomicValue source · line 189 · raw

Data

AtomicNull
```
AtomicValue
```
AtomicTrue
```
AtomicValue
```
AtomicFalse
```
AtomicValue
```

AtomicNumber

@text:String -> @certificate:0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.NumberCert<text> -> AtomicValue

AtomicString
```
@text:String -> AtomicValue
```

type SimpleValue source · line 196 · raw

Data

SimpleAtom
```
@atom:AtomicValue -> SimpleValue
```
SimpleEmptyArray
```
SimpleValue
```
SimpleEmptyObject
```
SimpleValue
```

type RenderMode source · line 215 · raw

Data

RenderWhole
```
RenderMode
```
RenderMembers
```
RenderMode
```
RenderAfterSeparator
```
RenderMode
```

type JsonPunctuation source · line 220 · raw

Data

ArrayEnd
```
JsonPunctuation
```
ObjectEnd
```
JsonPunctuation
```
MemberComma
```
JsonPunctuation
```
KeyColon
```
JsonPunctuation
```

Definitions

def token_source source · line 11 · raw

@xs:List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme> -> @tail:List<&1, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Token> -> List<&1, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Token>

def token_source_flat source · line 16 · raw

@+xs:List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme> -> @-tail:List<&1, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Token> -> {token_source(xs, tail) == 0xaca801afcf3e822677fd6d06895d2c71/proof/JSON_ParallelProof.flat(xs, tail) : List<&1, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Token>}

def is_members source · line 24 · raw

@mode:0xaca801afcf3e822677fd6d06895d2c71/proof/JSON_AssemblyProof.Mode -> Bool

def token_string source · line 29 · raw

@text:String -> 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Token

def nested_render_append source · line 32 · raw

@+outer:0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value -> @+inner:0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value -> @+inner_members:Bool -> @+prefix:String -> @+suffix:String -> @+outer_append:{String.append(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.render(outer, False{}, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.render(inner, inner_members, prefix)), suffix) == 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.render(outer, False{}, String.append(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.render(inner, inner_members, prefix), suffix)) : String} -> @+inner_append:{String.append(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.render(inner, inner_members, prefix), suffix) == 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.render(inner, inner_members, String.append(prefix, suffix)) : String} -> {String.append(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.render(outer, False{}, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.render(inner, inner_members, prefix)), suffix) == 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.render(outer, False{}, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.render(inner, inner_members, String.append(prefix, suffix))) : String}

def render_object_field_append source · line 50 · raw

@+prefix:String -> @+key:String -> @+text:String -> @+suffix:String -> {String.append(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.render_object_field(prefix, key, text), suffix) == 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.render_object_field(prefix, key, String.append(text, suffix)) : String}

def render_append source · line 56 · raw

@+value:0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value -> @+members:Bool -> @+prefix:String -> @+suffix:String -> {String.append(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.render(value, members, prefix), suffix) == 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.render(value, members, String.append(prefix, suffix)) : String}

def render_array_singleton_suffix source · line 149 · raw

@+head:0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value -> @+suffix:String -> {0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.render(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Arr{[head]}, False{}, suffix) == String.append("[", String.append(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.render(head, False{}, ""), String.append("]", suffix))) : String}

def lex_source_number_before_punctuation source · line 173 · raw

@+text:String -> @+certificate:0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.NumberCert<text> -> @+punctuation:Char -> @+suffix:String -> @+acc:List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme> -> @action:{0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_seed_action(SCon{punctuation, suffix}, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}) == 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.LexPunctuation{punctuation} : 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.LexAction} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_scan(String.append(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.render(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Number{text, certificate}, False{}, ""), String.append(SCon{punctuation, ""}, suffix)), 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}, "", acc) == 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_scan(suffix, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}, "", 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Punctuation{punctuation} <> 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Payload{text} <> acc) : List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme>}

def atomic_value source · line 201 · raw

@atom:AtomicValue -> 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value

def simple_value source · line 209 · raw

@simple:SimpleValue -> 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value

def punctuation_char source · line 226 · raw

@mark:JsonPunctuation -> Char

def punctuation_action source · line 233 · raw

@mark:JsonPunctuation -> @suffix:String -> {0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_seed_action(SCon{punctuation_char(mark), suffix}, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}) == 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.LexPunctuation{punctuation_char(mark)} : 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.LexAction}

def render_after_separator source · line 241 · raw

@value:0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value -> @suffix:String -> String

def render_task source · line 250 · raw

@value:0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value -> @mode:RenderMode -> @suffix:String -> String

def source_after_separator source · line 256 · raw

@value:0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value -> @suffix:List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme> -> List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme>

def source_task source · line 265 · raw

@value:0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value -> @mode:RenderMode -> @suffix:List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme> -> List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme>

def reverse_source_task source · line 271 · raw

@value:0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value -> @mode:RenderMode -> List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme>

def source_text_append source · line 274 · raw

@+text:String -> @+first:List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme> -> @+second:List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme> -> {0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.source_text(text, List.append(&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme, first, second)) == List.append(&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.source_text(text, first), second) : List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme>}

def source_append source · line 279 · raw

@+value:0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value -> @+members:Bool -> @+first:List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme> -> @+second:List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme> -> {0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.source(value, members, List.append(&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme, first, second)) == List.append(&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.source(value, members, first), second) : List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme>}

def reverse_source_suffix source · line 362 · raw

@+value:0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value -> @+members:Bool -> @+suffix:List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme> -> {List.reverse(&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.source(value, members, suffix)) == List.append(&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme, List.reverse(&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme, suffix), List.reverse(&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.source(value, members, []))) : List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme>}

def reverse_source_text source · line 376 · raw

@+text:String -> @+suffix:List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme> -> {List.reverse(&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.source_text(text, suffix)) == List.append(&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme, List.reverse(&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme, suffix), [0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Payload{text}]) : List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme>}

def reverse_source_colon_value_tail source · line 380 · raw

@+value:0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value -> @+tail:List<&2, Sigma<&2, &2, String, key => 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value>> -> {List.reverse(&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Punctuation{':'} <> 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.source(value, False{}, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.source(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Obj{tail}, True{}, []))) == List.append(&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme, reverse_source_task(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Obj{tail}, RenderMembers{}), List.append(&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme, reverse_source_task(value, RenderWhole{}), [0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Punctuation{':'}])) : List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme>}

def reverse_source_object_after_separator source · line 407 · raw

@+key:String -> @+value:0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value -> @+tail:List<&2, Sigma<&2, &2, String, key => 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value>> -> {reverse_source_task(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Obj{(key, value) <> tail}, RenderAfterSeparator{}) == List.append(&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme, reverse_source_task(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Obj{tail}, RenderMembers{}), List.append(&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme, reverse_source_task(value, RenderWhole{}), [0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Punctuation{':'}, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Payload{String.append("\"", String.append(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.escape_string(key), "\""))}])) : List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme>}

def reverse_source_object_members_after_separator source · line 462 · raw

@+key:String -> @+value:0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value -> @+tail:List<&2, Sigma<&2, &2, String, key => 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value>> -> {reverse_source_task(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Obj{(key, value) <> tail}, RenderMembers{}) == List.append(&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme, reverse_source_task(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Obj{(key, value) <> tail}, RenderAfterSeparator{}), [0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Punctuation{','}]) : List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme>}

def reverse_source_array_whole source · line 476 · raw

@+head:0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value -> @+tail:List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value> -> {reverse_source_task(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Arr{head <> tail}, RenderWhole{}) == List.append(&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme, reverse_source_task(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Arr{tail}, RenderMembers{}), List.append(&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme, reverse_source_task(head, RenderWhole{}), [0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Punctuation{'['}])) : List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme>}

def reverse_source_array_members source · line 505 · raw

@+head:0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value -> @+tail:List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value> -> {reverse_source_task(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Arr{head <> tail}, RenderMembers{}) == List.append(&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme, reverse_source_task(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Arr{tail}, RenderMembers{}), List.append(&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme, reverse_source_task(head, RenderWhole{}), [0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Punctuation{','}])) : List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme>}

def reverse_source_array_after_separator source · line 534 · raw

@+head:0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value -> @+tail:List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value> -> {reverse_source_task(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Arr{head <> tail}, RenderAfterSeparator{}) == List.append(&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme, reverse_source_task(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Arr{tail}, RenderMembers{}), reverse_source_task(head, RenderWhole{})) : List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme>}

def reverse_source_array_after_separator_whole source · line 538 · raw

@+head:0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value -> @+tail:List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value> -> {reverse_source_task(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Arr{head <> tail}, RenderWhole{}) == List.append(&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme, reverse_source_task(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Arr{head <> tail}, RenderAfterSeparator{}), [0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Punctuation{'['}]) : List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme>}

def reverse_source_array_members_after_separator source · line 569 · raw

@+head:0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value -> @+tail:List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value> -> {reverse_source_task(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Arr{head <> tail}, RenderMembers{}) == List.append(&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme, reverse_source_task(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Arr{head <> tail}, RenderAfterSeparator{}), [0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Punctuation{','}]) : List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme>}

def source_separator source · line 582 · raw

@value:0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value -> List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme>

def separator_text source · line 590 · raw

@value:0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value -> String

def render_members_decompose source · line 598 · raw

@+value:0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value -> @+suffix:String -> {0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.render(value, True{}, suffix) == String.append(separator_text(value), render_after_separator(value, suffix)) : String}

def render_after_separator_array_decompose source · line 613 · raw

@+head:0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value -> @+tail:List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value> -> @+suffix:String -> {render_after_separator(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Arr{head <> tail}, suffix) == String.append(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.render(head, False{}, ""), String.append(separator_text(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Arr{tail}), render_after_separator(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Arr{tail}, suffix))) : String}

def render_after_separator_object_decompose source · line 630 · raw

@+key:String -> @+value:0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value -> @+tail:List<&2, Sigma<&2, &2, String, key => 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value>> -> @+suffix:String -> {render_after_separator(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Obj{(key, value) <> tail}, suffix) == 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.render_object_field("", key, String.append(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.render(value, False{}, ""), String.append(separator_text(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Obj{tail}), render_after_separator(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Obj{tail}, suffix)))) : String}

def render_object_whole_decompose source · line 651 · raw

@+key:String -> @+value:0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value -> @+tail:List<&2, Sigma<&2, &2, String, key => 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value>> -> @+suffix:String -> {0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.render(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Obj{(key, value) <> tail}, False{}, suffix) == 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.render_object_field("{", key, String.append(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.render(value, False{}, ""), String.append(separator_text(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Obj{tail}), render_after_separator(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Obj{tail}, suffix)))) : String}

def render_array_whole_decompose source · line 672 · raw

@+head:0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value -> @+tail:List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value> -> @+suffix:String -> {0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.render(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Arr{head <> tail}, False{}, suffix) == String.append("[", String.append(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.render(head, False{}, ""), String.append(separator_text(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Arr{tail}), render_after_separator(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Arr{tail}, suffix)))) : String}

def render_after_separator_append source · line 681 · raw

@+value:0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value -> @+prefix:String -> @+suffix:String -> {String.append(render_after_separator(value, prefix), suffix) == render_after_separator(value, String.append(prefix, suffix)) : String}

def render_task_append source · line 714 · raw

@+value:0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value -> @+mode:RenderMode -> @+prefix:String -> @+suffix:String -> {String.append(render_task(value, mode, prefix), suffix) == render_task(value, mode, String.append(prefix, suffix)) : String}

def render_after_separator_array_single source · line 723 · raw

@+head:0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value -> @+suffix:String -> {render_after_separator(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Arr{[head]}, suffix) == render_task(head, RenderWhole{}, String.append("]", suffix)) : String}

def render_after_separator_array_many source · line 738 · raw

@+head:0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value -> @+next:0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value -> @+tail:List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value> -> @+suffix:String -> {render_after_separator(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Arr{head <> next <> tail}, suffix) == render_task(head, RenderWhole{}, String.append(",", render_after_separator(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Arr{next <> tail}, suffix))) : String}

def source_members_decompose source · line 753 · raw

@+value:0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value -> @+suffix:List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme> -> {0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.source(value, True{}, suffix) == List.append(&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme, source_separator(value), source_after_separator(value, suffix)) : List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme>}

def atomic_source source · line 768 · raw

@atom:AtomicValue -> List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme>

def atomic_source_reverse source · line 776 · raw

@+atom:AtomicValue -> {atomic_source(atom) == List.reverse(&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.source(atomic_value(atom), False{}, [])) : List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme>}

def lex_atomic_source_before_punctuation source · line 784 · raw

@+atom:AtomicValue -> @+punctuation:Char -> @+suffix:String -> @+acc:List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme> -> @action:{0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_seed_action(SCon{punctuation, suffix}, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}) == 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.LexPunctuation{punctuation} : 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.LexAction} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_scan(String.append(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.render(atomic_value(atom), False{}, ""), String.append(SCon{punctuation, ""}, suffix)), 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}, "", acc) == 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_scan(suffix, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}, "", 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Punctuation{punctuation} <> List.append(&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme, atomic_source(atom), acc)) : List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme>}

def lex_atomic_reverse_before_punctuation source · line 825 · raw

@+atom:AtomicValue -> @+punctuation:Char -> @+suffix:String -> @+acc:List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme> -> @action:{0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_seed_action(SCon{punctuation, suffix}, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}) == 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.LexPunctuation{punctuation} : 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.LexAction} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_scan(String.append(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.render(atomic_value(atom), False{}, ""), String.append(SCon{punctuation, ""}, suffix)), 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}, "", acc) == 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_scan(suffix, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}, "", 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Punctuation{punctuation} <> List.append(&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme, List.reverse(&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.source(atomic_value(atom), False{}, [])), acc)) : List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme>}

def lex_atomic_value_source source · line 840 · raw

@+atom:AtomicValue -> {0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_scan(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.stringify(atomic_value(atom)), 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}, "", []) == 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.source(atomic_value(atom), False{}, []) : List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme>}

def lex_source_empty_array_before_punctuation source · line 859 · raw

@+punctuation:Char -> @+suffix:String -> @+acc:List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme> -> @action:{0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_seed_action(SCon{punctuation, suffix}, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}) == 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.LexPunctuation{punctuation} : 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.LexAction} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_scan(String.append(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.render(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Arr{[]}, False{}, ""), String.append(SCon{punctuation, ""}, suffix)), 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}, "", acc) == 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_scan(suffix, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}, "", 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Punctuation{punctuation} <> 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Punctuation{']'} <> 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Punctuation{'['} <> acc) : List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme>}

def lex_source_empty_object_before_punctuation source · line 871 · raw

@+punctuation:Char -> @+suffix:String -> @+acc:List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme> -> @action:{0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_seed_action(SCon{punctuation, suffix}, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}) == 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.LexPunctuation{punctuation} : 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.LexAction} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_scan(String.append(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.render(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Obj{[]}, False{}, ""), String.append(SCon{punctuation, ""}, suffix)), 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}, "", acc) == 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_scan(suffix, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}, "", 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Punctuation{punctuation} <> 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Punctuation{'}'} <> 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Punctuation{'{'} <> acc) : List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme>}

def lex_empty_array_reverse_before_punctuation source · line 883 · raw

@+punctuation:Char -> @+suffix:String -> @+acc:List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme> -> @action:{0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_seed_action(SCon{punctuation, suffix}, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}) == 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.LexPunctuation{punctuation} : 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.LexAction} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_scan(String.append(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.render(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Arr{[]}, False{}, ""), String.append(SCon{punctuation, ""}, suffix)), 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}, "", acc) == 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_scan(suffix, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}, "", 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Punctuation{punctuation} <> List.append(&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme, List.reverse(&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.source(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Arr{[]}, False{}, [])), acc)) : List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme>}

def lex_empty_object_reverse_before_punctuation source · line 889 · raw

@+punctuation:Char -> @+suffix:String -> @+acc:List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme> -> @action:{0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_seed_action(SCon{punctuation, suffix}, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}) == 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.LexPunctuation{punctuation} : 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.LexAction} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_scan(String.append(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.render(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Obj{[]}, False{}, ""), String.append(SCon{punctuation, ""}, suffix)), 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}, "", acc) == 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_scan(suffix, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}, "", 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Punctuation{punctuation} <> List.append(&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme, List.reverse(&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.source(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Obj{[]}, False{}, [])), acc)) : List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme>}

def lex_simple_before_punctuation source · line 895 · raw

@+simple:SimpleValue -> @+punctuation:Char -> @+suffix:String -> @+acc:List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme> -> @action:{0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_seed_action(SCon{punctuation, suffix}, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}) == 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.LexPunctuation{punctuation} : 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.LexAction} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_scan(String.append(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.render(simple_value(simple), False{}, ""), String.append(SCon{punctuation, ""}, suffix)), 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}, "", acc) == 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_scan(suffix, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}, "", 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Punctuation{punctuation} <> List.append(&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme, List.reverse(&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.source(simple_value(simple), False{}, [])), acc)) : List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme>}

def lex_close_before_punctuation source · line 905 · raw

@+closing:Char -> @+punctuation:Char -> @+suffix:String -> @+acc:List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme> -> @close_action:{0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_seed_action(SCon{closing, String.append(SCon{punctuation, ""}, suffix)}, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}) == 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.LexPunctuation{closing} : 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.LexAction} -> @action:{0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_seed_action(SCon{punctuation, suffix}, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}) == 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.LexPunctuation{punctuation} : 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.LexAction} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_scan(SCon{closing, String.append(SCon{punctuation, ""}, suffix)}, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}, "", acc) == 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_scan(suffix, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}, "", 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Punctuation{punctuation} <> 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Punctuation{closing} <> acc) : List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme>}

def lex_object_key_before_colon source · line 918 · raw

@+key:String -> @+suffix:String -> @+acc:List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme> -> {0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_scan(String.append(String.append("\"", String.append(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.escape_string(key), "\"")), String.append(":", suffix)), 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}, "", acc) == 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_scan(suffix, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}, "", 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Punctuation{':'} <> 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Payload{String.append("\"", String.append(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.escape_string(key), "\""))} <> acc) : List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme>}

def atomic_task_render source · line 923 · raw

@atom:AtomicValue -> @mode:RenderMode -> {render_task(atomic_value(atom), mode, "") == 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.render(atomic_value(atom), False{}, "") : String}

def atomic_task_source source · line 942 · raw

@atom:AtomicValue -> @mode:RenderMode -> {reverse_source_task(atomic_value(atom), mode) == reverse_source_task(atomic_value(atom), RenderWhole{}) : List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme>}

def lex_atomic_task_before_punctuation source · line 961 · raw

@+atom:AtomicValue -> @+mode:RenderMode -> @+punctuation:Char -> @+suffix:String -> @+acc:List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme> -> @action:{0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_seed_action(SCon{punctuation, suffix}, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}) == 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.LexPunctuation{punctuation} : 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.LexAction} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_scan(String.append(render_task(atomic_value(atom), mode, ""), String.append(SCon{punctuation, ""}, suffix)), 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}, "", acc) == 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_scan(suffix, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}, "", 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Punctuation{punctuation} <> List.append(&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme, reverse_source_task(atomic_value(atom), mode), acc)) : List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme>}

def lex_simple_task_before_punctuation source · line 994 · raw

@+simple:SimpleValue -> @+mode:RenderMode -> @+punctuation:Char -> @+suffix:String -> @+acc:List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme> -> @action:{0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_seed_action(SCon{punctuation, suffix}, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}) == 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.LexPunctuation{punctuation} : 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.LexAction} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_scan(String.append(render_task(simple_value(simple), mode, ""), String.append(SCon{punctuation, ""}, suffix)), 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}, "", acc) == 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_scan(suffix, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}, "", 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Punctuation{punctuation} <> List.append(&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme, reverse_source_task(simple_value(simple), mode), acc)) : List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme>}

def lex_simple_task_suffix_before_punctuation source · line 1020 · raw

@+simple:SimpleValue -> @+mode:RenderMode -> @+punctuation:Char -> @+suffix:String -> @+acc:List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme> -> @action:{0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_seed_action(SCon{punctuation, suffix}, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}) == 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.LexPunctuation{punctuation} : 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.LexAction} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_scan(render_task(simple_value(simple), mode, String.append(SCon{punctuation, ""}, suffix)), 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}, "", acc) == 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_scan(suffix, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}, "", 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Punctuation{punctuation} <> List.append(&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme, reverse_source_task(simple_value(simple), mode), acc)) : List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme>}

def lex_array_singleton_value_before_punctuation source · line 1040 · raw

@+head:0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value -> @+punctuation:Char -> @+suffix:String -> @+acc:List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme> -> @action:{0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_seed_action(SCon{punctuation, suffix}, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}) == 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.LexPunctuation{punctuation} : 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.LexAction} -> @head_lex:{0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_scan(String.append(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.render(head, False{}, ""), SCon{']', String.append(SCon{punctuation, ""}, suffix)}), 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}, "", 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Punctuation{'['} <> acc) == 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_scan(String.append(SCon{punctuation, ""}, suffix), 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}, "", 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Punctuation{']'} <> List.append(&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme, reverse_source_task(head, RenderWhole{}), 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Punctuation{'['} <> acc)) : List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme>} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_scan(String.append(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.render(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Arr{[head]}, False{}, ""), String.append(SCon{punctuation, ""}, suffix)), 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}, "", acc) == 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_scan(suffix, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}, "", 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Punctuation{punctuation} <> 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Punctuation{']'} <> List.append(&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme, reverse_source_task(head, RenderWhole{}), 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Punctuation{'['} <> acc)) : List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme>}

def lex_array_singleton_before_punctuation source · line 1079 · raw

@+head:SimpleValue -> @+punctuation:Char -> @+suffix:String -> @+acc:List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme> -> @action:{0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_seed_action(SCon{punctuation, suffix}, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}) == 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.LexPunctuation{punctuation} : 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.LexAction} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_scan(String.append(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.render(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Arr{[simple_value(head)]}, False{}, ""), String.append(SCon{punctuation, ""}, suffix)), 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}, "", acc) == 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_scan(suffix, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}, "", 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Punctuation{punctuation} <> 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Punctuation{']'} <> List.append(&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme, reverse_source_task(simple_value(head), RenderWhole{}), 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Punctuation{'['} <> acc)) : List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme>}

def lex_array_after_separator_single source · line 1088 · raw

@+head:0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value -> @+punctuation:Char -> @+suffix:String -> @+acc:List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme> -> @action:{0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_seed_action(SCon{punctuation, suffix}, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}) == 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.LexPunctuation{punctuation} : 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.LexAction} -> @head_lex:{0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_scan(render_task(head, RenderWhole{}, String.append("]", String.append(SCon{punctuation, ""}, suffix))), 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}, "", acc) == 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_scan(String.append(SCon{punctuation, ""}, suffix), 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}, "", 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Punctuation{']'} <> List.append(&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme, reverse_source_task(head, RenderWhole{}), acc)) : List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme>} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_scan(render_after_separator(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Arr{[head]}, String.append(SCon{punctuation, ""}, suffix)), 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}, "", acc) == 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_scan(suffix, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}, "", 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Punctuation{punctuation} <> 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Punctuation{']'} <> List.append(&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme, reverse_source_task(head, RenderWhole{}), acc)) : List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme>}

def lex_array_after_separator_single_source source · line 1117 · raw

@+head:0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value -> @+punctuation:Char -> @+suffix:String -> @+acc:List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme> -> @action:{0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_seed_action(SCon{punctuation, suffix}, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}) == 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.LexPunctuation{punctuation} : 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.LexAction} -> @head_lex:{0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_scan(render_task(head, RenderWhole{}, String.append("]", String.append(SCon{punctuation, ""}, suffix))), 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}, "", acc) == 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_scan(String.append(SCon{punctuation, ""}, suffix), 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}, "", 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Punctuation{']'} <> List.append(&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme, reverse_source_task(head, RenderWhole{}), acc)) : List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme>} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_scan(render_after_separator(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Arr{[head]}, String.append(SCon{punctuation, ""}, suffix)), 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}, "", acc) == 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_scan(suffix, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}, "", 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Punctuation{punctuation} <> List.append(&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme, reverse_source_task(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Arr{[head]}, RenderAfterSeparator{}), acc)) : List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme>}

def reverse_array_after_separator_acc_many source · line 1139 · raw

@+head:0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value -> @+next:0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value -> @+tail:List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value> -> @+acc:List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme> -> {List.append(&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme, reverse_source_task(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Arr{next <> tail}, RenderAfterSeparator{}), 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Punctuation{','} <> List.append(&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme, reverse_source_task(head, RenderWhole{}), acc)) == List.append(&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme, reverse_source_task(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Arr{head <> next <> tail}, RenderAfterSeparator{}), acc) : List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme>}

def lex_array_after_separator_many source · line 1195 · raw

@+head:0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value -> @+next:0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value -> @+tail:List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value> -> @+punctuation:Char -> @+suffix:String -> @+acc:List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme> -> @action:{0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_seed_action(SCon{punctuation, suffix}, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}) == 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.LexPunctuation{punctuation} : 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.LexAction} -> @head_lex:{0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_scan(render_task(head, RenderWhole{}, String.append(",", render_after_separator(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Arr{next <> tail}, String.append(SCon{punctuation, ""}, suffix)))), 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}, "", acc) == 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_scan(render_after_separator(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Arr{next <> tail}, String.append(SCon{punctuation, ""}, suffix)), 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}, "", 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Punctuation{','} <> List.append(&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme, reverse_source_task(head, RenderWhole{}), acc)) : List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme>} -> @tail_lex:{0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_scan(render_after_separator(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Arr{next <> tail}, String.append(SCon{punctuation, ""}, suffix)), 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}, "", 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Punctuation{','} <> List.append(&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme, reverse_source_task(head, RenderWhole{}), acc)) == 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_scan(suffix, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}, "", 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Punctuation{punctuation} <> List.append(&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme, reverse_source_task(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Arr{next <> tail}, RenderAfterSeparator{}), 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Punctuation{','} <> List.append(&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme, reverse_source_task(head, RenderWhole{}), acc))) : List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme>} -> {0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_scan(render_after_separator(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Arr{head <> next <> tail}, String.append(SCon{punctuation, ""}, suffix)), 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}, "", acc) == 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_scan(suffix, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}, "", 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Punctuation{punctuation} <> List.append(&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme, reverse_source_task(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Arr{head <> next <> tail}, RenderAfterSeparator{}), acc)) : List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme>}

def lex_array_after_separator_two_simple source · line 1238 · raw

@+first:SimpleValue -> @+second:SimpleValue -> @+mark:JsonPunctuation -> @+suffix:String -> @+acc:List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme> -> {0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_scan(render_after_separator(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Arr{[simple_value(first), simple_value(second)]}, String.append(SCon{punctuation_char(mark), ""}, suffix)), 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}, "", acc) == 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_scan(suffix, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}, "", 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Punctuation{punctuation_char(mark)} <> List.append(&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme, reverse_source_task(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Arr{[simple_value(first), simple_value(second)]}, RenderAfterSeparator{}), acc)) : List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme>}

def simple_values source · line 1268 · raw

@values:List<&2, SimpleValue> -> List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value>

def lex_simple_array_after_separator_end source · line 1273 · raw

@+values:List<&2, SimpleValue> -> @+acc:List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme> -> {0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_scan(render_after_separator(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Arr{simple_values(values)}, ""), 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}, "", acc) == 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_scan("", 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}, "", List.append(&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme, reverse_source_task(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Arr{simple_values(values)}, RenderAfterSeparator{}), acc)) : List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme>}

def reverse_source_array_after_separator_whole_list source · line 1338 · raw

@+values:List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value> -> {reverse_source_task(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Arr{values}, RenderWhole{}) == List.append(&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme, reverse_source_task(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Arr{values}, RenderAfterSeparator{}), [0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Punctuation{'['}]) : List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme>}

def render_array_whole_after_separator source · line 1343 · raw

@+values:List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value> -> @+suffix:String -> {0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.render(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Arr{values}, False{}, suffix) == String.append("[", render_after_separator(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Arr{values}, suffix)) : String}

def lex_simple_array_whole source · line 1349 · raw

@+values:List<&2, SimpleValue> -> {0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_scan(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.render(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Arr{simple_values(values)}, False{}, ""), 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}, "", []) == 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.source(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Arr{simple_values(values)}, False{}, []) : List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme>}

def lex_simple_array_after_separator source · line 1382 · raw

@+values:List<&2, SimpleValue> -> @+mark:JsonPunctuation -> @+suffix:String -> @+acc:List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme> -> {0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_scan(render_after_separator(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Arr{simple_values(values)}, String.append(SCon{punctuation_char(mark), ""}, suffix)), 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}, "", acc) == 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.lex_scan(suffix, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Outside{}, "", 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Punctuation{punctuation_char(mark)} <> List.append(&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme, reverse_source_task(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Arr{simple_values(values)}, RenderAfterSeparator{}), acc)) : List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme>}

def source_token_string source · line 1402 · raw

@+text:String -> @+suffix:List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme> -> @-tail:List<&1, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Token> -> {token_source(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.source_text(String.append("\"", String.append(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.escape_string(text), "\"")), suffix), tail) == token_string(text) <> token_source(suffix, tail) : List<&1, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Token>}

def source_object_key_prefix source · line 1408 · raw

@+delimiter:Char -> @+key:String -> @+suffix:List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme> -> @-tail:List<&1, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Token> -> {token_source(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Punctuation{delimiter} <> 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.source_text(String.append("\"", String.append(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.escape_string(key), "\"")), suffix), tail) == 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Delimiter{delimiter} <> token_string(key) <> token_source(suffix, tail) : List<&1, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Token>}

def to_bool source · line 1421 · raw

@mode:0xaca801afcf3e822677fd6d06895d2c71/proof/JSON_AssemblyProof.Mode -> Bool

def canonical source · line 1426 · raw

@value:0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value -> @mode:0xaca801afcf3e822677fd6d06895d2c71/proof/JSON_AssemblyProof.Mode -> @tail:List<&1, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Token> -> List<&1, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Token>

def canonical_tokens source · line 1429 · raw

@+value:0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value -> @+mode:0xaca801afcf3e822677fd6d06895d2c71/proof/JSON_AssemblyProof.Mode -> @-tail:List<&1, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Token> -> {canonical(value, mode, tail) == 0xaca801afcf3e822677fd6d06895d2c71/proof/JSON_AssemblyProof.tokens(value, mode, tail) : List<&1, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Token>}

def source_tokens source · line 1434 · raw

@+value:0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Value -> @+mode:0xaca801afcf3e822677fd6d06895d2c71/proof/JSON_AssemblyProof.Mode -> @+suffix:List<&2, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Lexeme> -> @-tail:List<&1, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Token> -> {token_source(0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.source(value, to_bool(mode), suffix), tail) == canonical(value, mode, token_source(suffix, tail)) : List<&1, 0xaca801afcf3e822677fd6d06895d2c71/libs/JSON.Token>}