proof/JSON_StringProof.bend checks

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

3 imports

import Base
import ../libs/JSON.bend as J
import ./JSON_PrimitiveProof.bend as P

Definitions

def append_nil source · line 5

@+text:String -> {String.append(text, "") == text : String}

def append_assoc source · line 11

@+a:String -> @+b:String -> @+c:String -> {String.append(String.append(a, b), c) == String.append(a, String.append(b, c)) : String}

def reverse_go_append source · line 17

@+text:String -> @+acc:String -> @+suffix:String -> {String.reverse.go(text, String.append(acc, suffix)) == String.append(String.reverse.go(text, acc), suffix) : String}

def reverse_cons source · line 30

@+head:Char -> @+tail:String -> {String.reverse(SCon{head, tail}) == String.append(String.reverse(tail), SCon{head, ""}) : String}

def reverse_append source · line 34

@+left:String -> @+right:String -> {String.reverse(String.append(left, right)) == String.append(String.reverse(right), String.reverse(left)) : String}

def reverse_twice source · line 57

@+text:String -> {String.reverse(String.reverse(text)) == text : String}

def escape_one source · line 69

@+c:Char -> @+tail:String -> @+value:String -> @evidence:{0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.fast_string(tail) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Decoded{value} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.FastString} -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.fast_string(String.append(0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.escape_char(c), tail)) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Decoded{SCon{c, value}} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.FastString}

def escaped_body source · line 1969

@+text:String -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.fast_string(String.append(0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.escape_string(text), "\"")) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Decoded{text} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.FastString}

def number_quote source · line 1977

@+text:String -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.number_valid(SCon{'"', text}) == False{} : Bool}

def string_payload source · line 1980

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