proof/JSON_PrimitiveProof.bend checks

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

2 imports

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

Definitions

def R source · line 4 · raw

Type

def absurd source · line 7 · raw

@-A:Type -> @empty:Empty -> A

def false_type source · line 10 · raw

@b:Bool -> Data

def false_true source · line 15 · raw

@e:{False{} == True{} : Bool} -> Empty

def proof_valid source · line 19 · raw

@+valid:Bool -> @witness:0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.NumberProofFrom(valid) -> {valid == True{} : Bool}

def cert_valid source · line 25 · raw

@+text:String -> @certificate:0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.NumberCert<text> -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.number_valid(text) == True{} : Bool}

def proof_unique source · line 30 · raw

@+valid:Bool -> @+a:0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.NumberProofFrom(valid) -> @+b:0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.NumberProofFrom(valid) -> {a == b : 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.NumberProofFrom(valid)}

def cert_unique source · line 40 · raw

@+text:String -> @+a:0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.NumberCert<text> -> @+b:0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.NumberCert<text> -> {a == b : 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.NumberCert<text>}

def number_route source · line 47 · raw

@+text:String -> @+valid:Bool -> @+certificate:0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.NumberCert<text> -> @evidence:{0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.number_valid(text) == valid : Bool} -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.payload_number(text, valid, evidence) == Done{0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.Number{text, certificate}} : R}

def number_roundtrip source · line 61 · raw

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

def invalid_step source · line 65 · raw

@+text:String -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.number_valid_step(text, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.NumberInvalid{}) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.NumberInvalid{} : 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.NumberState}

def route_false source · line 70 · raw

@+text:String -> @+valid:Bool -> @evidence:{0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.number_valid(text) == valid : Bool} -> @no:{valid == False{} : Bool} -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.payload_number(text, valid, evidence) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.payload_other(text) : R}

def decode_false source · line 79 · raw

@+text:String -> @no:{0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.number_valid(text) == False{} : Bool} -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.decode_payload(text) == 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.payload_other(text) : R}

def invalid_end source · line 83 · raw

@+text:String -> {0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.number_valid_end(0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.number_valid_step(text, 0x3d2147650fe101ae3c3e4a95333b4238/libs/JSON.NumberInvalid{})) == False{} : Bool}