~/bend-docscommunity

proofs/lib/links.bend checks

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

10 imports
import Base
import ../../src/containers/hash_table.bend as H
import ./u32.bend as UW
import ../../spec/lib/common.bend as SC
import ./nat_list.bend as NL
import ./logic.bend as L
import ./nat.bend as N
import ./u32div.bend as UD
import ./words32.bend as W32
import ./word.bend as WD

Definitions

def lnk source · line 16 · raw

@+s:Nat -> U32

def fst_or source · line 19 · raw

@t:List<&2, Nat> -> @+q:U32 -> U32

def last_or source · line 26 · raw

@t:List<&2, Nat> -> @+p:U32 -> U32

def u_refl source · line 33 · raw

@+x:U32 -> {U32.is_eq(x, x) == True{} : Bool}

def fst_app source · line 36 · raw

@+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+q:U32 -> {fst_or(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b), q) == fst_or(a, fst_or(b, q)) : U32}

def last_app source · line 43 · raw

@+a:List<&2, Nat> -> @+b:List<&2, Nat> -> @+p:U32 -> {last_or(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Nat, a, b), p) == last_or(b, last_or(a, p)) : U32}

def last_lnk source · line 50 · raw

@+t:List<&2, Nat> -> @+a:Nat -> {last_or(t, lnk(a)) == lnk(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.lastn(t, a)) : U32}

def fo_rapp source · line 57 · raw

@+l:List<&2, Nat> -> @+b:List<&2, Nat> -> @+d:U32 -> {fst_or(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/nat_list.rapp(l, b), d) == last_or(l, fst_or(b, d)) : U32}

def slot_lnk source · line 69 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+s:Nat -> @+sd:Nat -> @+hsd:{Nat.is_lt(1n+sd, 32n) == True{} : Bool} -> @+hs:{Nat.is_lt(s, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(sd)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/u32div.v(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/hash_table.slot(lnk(s))) == s : Nat}