proofs/lib/array_ext.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/lib/array_ext.bend as Array_ext

6 imports

import Base
import ./logic.bend as L
import ./nat.bend as N
import ./list.bend as LL
import ./array.bend as AR
import ../../spec/lib/common.bend as SC

Definitions

def take_len source · line 11 · raw

@-A:Data -> @+xs:List<&2, A> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(A, xs, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(A, xs)) == xs : List<&2, A>}

def drop_zero source · line 18 · raw

@-A:Data -> @+xs:List<&2, A> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.drop(A, xs, 0n) == xs : List<&2, A>}

def take_app_len source · line 25 · raw

@-A:Data -> @+xs:List<&2, A> -> @+ys:List<&2, A> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(A, xs, ys), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(A, xs)) == xs : List<&2, A>}

def drop_app_len source · line 28 · raw

@-A:Data -> @+xs:List<&2, A> -> @+ys:List<&2, A> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.drop(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(A, xs, ys), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(A, xs)) == ys : List<&2, A>}

def split_eq source · line 35 · raw

@-A:Data -> @+a1:List<&2, A> -> @+b1:List<&2, A> -> @+a2:List<&2, A> -> @+b2:List<&2, A> -> @+el:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(A, a1) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(A, a2) : Nat} -> @+e:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(A, a1, b1) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(A, a2, b2) : List<&2, A>} -> {a1 == a2 : List<&2, A>}

def split_eq_r source · line 39 · raw

@-A:Data -> @+a1:List<&2, A> -> @+b1:List<&2, A> -> @+a2:List<&2, A> -> @+b2:List<&2, A> -> @+el:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(A, a1) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(A, a2) : Nat} -> @+e:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(A, a1, b1) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(A, a2, b2) : List<&2, A>} -> {b1 == b2 : List<&2, A>}

def head_of source · line 43 · raw

@-A:Data -> @xs:List<&2, A> -> @+d:A -> A

def tree_ext source · line 50 · raw

@-A:Data -> @+d:Nat -> @+u:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<A> -> @+v:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<A> -> @+pu:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(A, d, u) == True{} : Bool} -> @+pv:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(A, d, v) == True{} : Bool} -> @+e:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(A, u) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(A, v) : List<&2, A>} -> {u == v : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<A>}