~/bend-docscommunity

PROOF.bend checks

raw source on the hub · import qasim-bend-kit@0.1.0.0/PROOF.bend as PROOF

12 imports
import Base
import ./LAWS.bend as L
import ./libs/JSON.bend as Json
import ./libs/URL.bend as URL
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

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 -> {0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.assemble([0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Atom{result}], 0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.NeedValue{0x0b4f68372ee8cbe03f4a66931f85cfdc/libs/JSON.Top{}}) == result : ResultValue}

def parallel_single source · line 25 · raw

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

def assemble_source source · line 30 · raw

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

def parse_number_payload source · line 57 · raw

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

def assembled_string_payload source · line 82 · raw

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

def parse_string_payload source · line 86 · raw

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

def parse_leading_space source · line 104 · raw

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

def parse_trailing_space source · line 107 · raw

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

def parse_trailing_tab source · line 114 · raw

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

def parse_trailing_return source · line 121 · raw

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

def parse_trailing_newline source · line 128 · raw

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

def parse_suffix_space source · line 135 · raw

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

def parse_suffix_tab source · line 142 · raw

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

def parse_suffix_return source · line 149 · raw

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

def parse_suffix_newline source · line 156 · raw

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

def parse_leading_surround source · line 163 · raw

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

def parse_surrounding_space source · line 166 · raw

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