~/bend-docscommunity

PROOF.bend fails

raw source on the hub · import 0x3d2147650fe101ae3c3e4a95333b4238/PROOF.bend as PROOF

12 imports
import Base
import ./LAWS.bend as L
import ./libs/JSON.bend as Json
import ./proof/JSON_StringProof.bend as StringProof
import ./proof/JSON_PrimitiveProof.bend as PrimitiveProof
import ./proof/JSON_NumberLexProof.bend as NumberLexProof
import ./proof/JSON_ParallelProof.bend as ParallelProof
import ./proof/JSON_LexWhitespaceProof.bend as LexWhitespaceProof
import ./proof/JSON_AssemblyProof.bend as AssemblyProof
import ./proof/JSON_SourceProof.bend as SourceProof
import ./proof/JSON_RenderLexProof.bend as RenderLexProof
import ./proof/HTTPClientProof.bend as HttpProof

Definitions

def ResultValue source · line 14 · raw

Type

def parse_for_equality source · line 17 · raw

@text:String -> ResultValue

def assemble_atom source · line 20 · raw

@result:ResultValue -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.assemble([0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Atom{result}], 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.NeedValue{0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Top{}}) == result : ResultValue}

def parallel_single source · line 25 · raw

@+text:String -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.token_list(0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.decode_tree(0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.lex_tree([0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Payload{text}])), []) == [0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.decode_lexeme(0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Payload{text})] : List<&1, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Token>}

def assemble_source source · line 30 · raw

@+value:0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Value -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.assemble(0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.token_list(0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.decode_tree(0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.lex_tree(0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.source(value, False{}, []))), []), 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.NeedValue{0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Top{}}) == Done{value} : ResultValue}

def parse_number_payload source · line 57 · raw

@+text:String -> @+certificate:0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.NumberCert<text> -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.parse_normalized(text) == Done{0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Number{text, certificate}} : ResultValue}

def assembled_string_payload source · line 82 · raw

@+text:String -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.assemble([0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Atom{0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.decode_payload(String.append("\"", String.append(0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.escape_string(text), "\"")))}], 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.NeedValue{0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Top{}}) == Done{0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Str{text}} : ResultValue}

def parse_string_payload source · line 86 · raw

@+text:String -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.parse_normalized(String.append("\"", String.append(0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.escape_string(text), "\""))) == Done{0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Str{text}} : ResultValue}

def parse_leading_space source · line 104 · raw

@+text:String -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.parse(String.append(" ", text)) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.parse(text) : Result<&1, &1, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Error, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Value>}

def parse_trailing_space source · line 107 · raw

@+text:String -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.parse(String.append(text, " ")) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.parse(text) : Result<&1, &1, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Error, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Value>}

def parse_trailing_tab source · line 114 · raw

@+text:String -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.parse(String.append(text, "\t")) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.parse(text) : Result<&1, &1, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Error, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Value>}

def parse_trailing_return source · line 121 · raw

@+text:String -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.parse(String.append(text, "\r")) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.parse(text) : Result<&1, &1, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Error, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Value>}

def parse_trailing_newline source · line 128 · raw

@+text:String -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.parse(String.append(text, "\n")) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.parse(text) : Result<&1, &1, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Error, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Value>}

def parse_suffix_space source · line 135 · raw

@+text:String -> @+suffix:String -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.parse(String.append(text, String.append(suffix, " "))) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.parse(String.append(text, suffix)) : Result<&1, &1, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Error, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Value>}

def parse_suffix_tab source · line 142 · raw

@+text:String -> @+suffix:String -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.parse(String.append(text, String.append(suffix, "\t"))) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.parse(String.append(text, suffix)) : Result<&1, &1, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Error, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Value>}

def parse_suffix_return source · line 149 · raw

@+text:String -> @+suffix:String -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.parse(String.append(text, String.append(suffix, "\r"))) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.parse(String.append(text, suffix)) : Result<&1, &1, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Error, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Value>}

def parse_suffix_newline source · line 156 · raw

@+text:String -> @+suffix:String -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.parse(String.append(text, String.append(suffix, "\n"))) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.parse(String.append(text, suffix)) : Result<&1, &1, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Error, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Value>}

def parse_leading_surround source · line 163 · raw

@+text:String -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.parse(String.append(" \n\t\r", text)) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.parse(text) : Result<&1, &1, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Error, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Value>}

def parse_surrounding_space source · line 166 · raw

@+text:String -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.parse(String.append(" \n\t\r", String.append(text, "\r\t\n "))) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.parse(text) : Result<&1, &1, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Error, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Value>}