proofs/containers/bitset/listx.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitset/listx.bend as Listx

5 imports

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

Definitions

def take_zero source · line 10 · raw

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

def drop_zero source · line 17 · raw

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

def drop_cons source · line 25 · raw

@-A:Data -> @xs:List<&2, A> -> @q:Nat -> @+x:A -> @+hx:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(A, xs, q) == Some{x} : Maybe<&2, A>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.drop(A, xs, q) == x <> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.drop(A, xs, 1n+q) : List<&2, A>}

The element at q, pulled out of the tail that starts there.

def take_succ source · line 37 · raw

@-A:Data -> @xs:List<&2, A> -> @q:Nat -> @+x:A -> @+hx:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(A, xs, q) == Some{x} : Maybe<&2, A>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(A, xs, 1n+q) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(A, xs, q), x) : List<&2, A>}

One more element taken is that element appended.

def drop_update source · line 49 · raw

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

Replacing position q does not disturb what follows it.

def take_update source · line 59 · raw

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

... nor what precedes it.

def take_update_succ source · line 68 · raw

@-A:Data -> @xs:List<&2, A> -> @q:Nat -> @+v:A -> @+h:{Nat.is_lt(q, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(A, xs)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(A, xs, q, v), 1n+q) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(A, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(A, xs, q), v) : List<&2, A>}

def take_all source · line 78 · 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_all source · line 85 · raw

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