proof/JSON_ListProof.bend checks

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

1 import

import Base

Definitions

def append_nil source · line 3 · raw

@-A:Data -> @+xs:List<&2, A> -> {List.append(&2, A, xs, []) == xs : List<&2, A>}

def append_assoc source · line 9 · raw

@-A:Data -> @+xs:List<&2, A> -> @+ys:List<&2, A> -> @+zs:List<&2, A> -> {List.append(&2, A, List.append(&2, A, xs, ys), zs) == List.append(&2, A, xs, List.append(&2, A, ys, zs)) : List<&2, A>}

def reverse_shift source · line 19 · raw

@-A:Data -> @+xs:List<&2, A> -> @+acc:List<&2, A> -> @+tail:List<&2, A> -> {List.reverse.go(&2, A, List.reverse.go(&2, A, xs, acc), tail) == List.reverse.go(&2, A, acc, List.append(&2, A, xs, tail)) : List<&2, A>}

def reverse_go_append source · line 27 · raw

@-A:Data -> @+xs:List<&2, A> -> @+acc:List<&2, A> -> @+tail:List<&2, A> -> {List.reverse.go(&2, A, xs, List.append(&2, A, acc, tail)) == List.append(&2, A, List.reverse.go(&2, A, xs, acc), tail) : List<&2, A>}

def reverse_cons source · line 36 · raw

@-A:Data -> @+head:A -> @+tail:List<&2, A> -> {List.reverse(&2, A, head <> tail) == List.append(&2, A, List.reverse(&2, A, tail), [head]) : List<&2, A>}

def reverse_append source · line 41 · raw

@-A:Data -> @+xs:List<&2, A> -> @+ys:List<&2, A> -> {List.reverse(&2, A, List.append(&2, A, xs, ys)) == List.append(&2, A, List.reverse(&2, A, ys), List.reverse(&2, A, xs)) : List<&2, A>}

def reverse_twice source · line 76 · raw

@-A:Data -> @+xs:List<&2, A> -> {List.reverse(&2, A, List.reverse(&2, A, xs)) == xs : List<&2, A>}