spec/containers/bitset.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/spec/containers/bitset.bend as Bitset

3 imports

import Base
import ../lib/common.bend as C
import ../../src/containers/types/bitset.bend as E

Definitions

def new source · line 8 · raw

@n:Nat -> List<&2, Bool>

def count source · line 12 · raw

@xs:List<&2, Bool> -> Nat

Number of True bits.

def members source · line 22 · raw

@xs:List<&2, Bool> -> @+off:Nat -> List<&2, Nat>

Indices (offset by off) of True bits, ascending.

def zip_or source · line 32 · raw

@xs:List<&2, Bool> -> @ys:List<&2, Bool> -> List<&2, Bool>

Element-wise combination of two sequences (truncates to the shorter one).

def zip_and source · line 39 · raw

@xs:List<&2, Bool> -> @ys:List<&2, Bool> -> List<&2, Bool>

def zip_diff source · line 46 · raw

@xs:List<&2, Bool> -> @ys:List<&2, Bool> -> List<&2, Bool>

def zip_xor source · line 53 · raw

@xs:List<&2, Bool> -> @ys:List<&2, Bool> -> List<&2, Bool>

def bit source · line 60 · raw

@x:Maybe<&2, Bool> -> Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Error, Bool>

def get source · line 67 · raw

@xs:List<&2, Bool> -> @i:Nat -> Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Error, Bool>

def assign_at source · line 71 · raw

@x:Maybe<&2, Bool> -> @+xs:List<&2, Bool> -> @i:Nat -> @v:Bool -> Pair(List<&2, Bool>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Obs)

Assign bit i; out of range leaves the sequence unchanged and fails.

def assign source · line 78 · raw

@+xs:List<&2, Bool> -> @+i:Nat -> @v:Bool -> Pair(List<&2, Bool>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Obs)

def combine_if source · line 83 · raw

@same:Bool -> @xs:List<&2, Bool> -> @r:List<&2, Bool> -> Pair(List<&2, Bool>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Obs)

Combine with an operand of the same logical size; a size mismatch leaves the sequence unchanged and fails.

def combine source · line 90 · raw

@+xs:List<&2, Bool> -> @ys:List<&2, Bool> -> @r:List<&2, Bool> -> Pair(List<&2, Bool>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Obs)

def step source · line 93 · raw

@+xs:List<&2, Bool> -> @op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Op -> Pair(List<&2, Bool>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Obs)

def cons_obs source · line 116 · raw

@o:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Obs -> @r:Pair(List<&2, Bool>, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Obs>) -> Pair(List<&2, Bool>, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Obs>)

def run source · line 120 · raw

@ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Op> -> @+xs:List<&2, Bool> -> Pair(List<&2, Bool>, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Obs>)

def ins source · line 170 · raw

@x:Maybe<&2, Bool> -> Bool

def inset source · line 178 · raw

@xs:List<&2, Bool> -> @k:Nat -> Bool

Contains (Model, k)

def nx source · line 181 · raw

@+xs:List<&2, Bool> -> @+op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Op -> List<&2, Bool>

def ob source · line 184 · raw

@+xs:List<&2, Bool> -> @+op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Op -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Obs

def nmem source · line 188 · raw

@+k:Nat -> @ys:List<&2, Nat> -> Bool

---- Elements: to_list is the ascending sequence of the members ----

def Contains.get_result source · line 196 · raw

@+xs:List<&2, Bool> -> @+i:Nat -> @+h:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs)) == True{} : Bool} -> Type

Contains (1717)

def Contains.get_frame source · line 200 · raw

@+xs:List<&2, Bool> -> @+i:Nat -> Type

Contains (1717)

def Contains.get_outside source · line 204 · raw

@+xs:List<&2, Bool> -> @+i:Nat -> @+h:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs), i) == True{} : Bool} -> Type

Contains (1717)

def Length.count_result source · line 208 · raw

@+xs:List<&2, Bool> -> Type

Length (112)

def Length.count_frame source · line 212 · raw

@+xs:List<&2, Bool> -> Type

Length (112)

def Capacity.length_result source · line 216 · raw

@+xs:List<&2, Bool> -> Type

Capacity

def Capacity.length_frame source · line 220 · raw

@+xs:List<&2, Bool> -> Type

Capacity

def Empty_Set.new_contains source · line 224 · raw

@+n:Nat -> @+k:Nat -> Type

Empty_Set (99)

def Empty_Set.new_count source · line 228 · raw

@+n:Nat -> Type

Empty_Set (99)

def Empty_Set.new_length source · line 232 · raw

@+n:Nat -> Type

Empty_Set (99)

def Include.set_contains source · line 236 · raw

@+xs:List<&2, Bool> -> @+i:Nat -> @+h:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs)) == True{} : Bool} -> Type

Include (831) / Insert (777)

def Include.set_others source · line 240 · raw

@+xs:List<&2, Bool> -> @+i:Nat -> @+h:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs)) == True{} : Bool} -> @+j:Nat -> @+ne:{Nat.is_eq(i, j) == False{} : Bool} -> Type

Include (831) / Insert (777)

def Include.set_universe source · line 244 · raw

@+xs:List<&2, Bool> -> @+i:Nat -> @+h:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs)) == True{} : Bool} -> Type

Include (831) / Insert (777)

def Include.set_outside source · line 248 · raw

@+xs:List<&2, Bool> -> @+i:Nat -> @+h:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs), i) == True{} : Bool} -> Type

Include (831) / Insert (777)

def Exclude.clear_contains source · line 252 · raw

@+xs:List<&2, Bool> -> @+i:Nat -> @+h:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs)) == True{} : Bool} -> Type

Exclude (953) / Delete (1051)

def Exclude.clear_others source · line 256 · raw

@+xs:List<&2, Bool> -> @+i:Nat -> @+h:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs)) == True{} : Bool} -> @+j:Nat -> @+ne:{Nat.is_eq(i, j) == False{} : Bool} -> Type

Exclude (953) / Delete (1051)

def Exclude.clear_universe source · line 260 · raw

@+xs:List<&2, Bool> -> @+i:Nat -> @+h:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs)) == True{} : Bool} -> Type

Exclude (953) / Delete (1051)

def Exclude.clear_outside source · line 264 · raw

@+xs:List<&2, Bool> -> @+i:Nat -> @+h:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs), i) == True{} : Bool} -> Type

Exclude (953) / Delete (1051)

def Include.set_count source · line 268 · raw

@+xs:List<&2, Bool> -> @+i:Nat -> @+h:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs)) == True{} : Bool} -> Type

Include (831) / Insert (777)

def Exclude.clear_count source · line 272 · raw

@+xs:List<&2, Bool> -> @+i:Nat -> @+h:{Nat.is_lt(i, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs)) == True{} : Bool} -> Type

Exclude (953) / Delete (1051)

def Union.union_contains source · line 276 · raw

@+xs:List<&2, Bool> -> @+ys:List<&2, Bool> -> @+k:Nat -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, ys) : Nat} -> Type

Union (1235)

def Union.union_mismatch source · line 280 · raw

@+xs:List<&2, Bool> -> @+ys:List<&2, Bool> -> @+h:{Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, ys)) == False{} : Bool} -> Type

Union (1235)

def Intersection.intersection_contains source · line 284 · raw

@+xs:List<&2, Bool> -> @+ys:List<&2, Bool> -> @+k:Nat -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, ys) : Nat} -> Type

Intersection (1307)

def Intersection.intersection_mismatch source · line 288 · raw

@+xs:List<&2, Bool> -> @+ys:List<&2, Bool> -> @+h:{Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, ys)) == False{} : Bool} -> Type

Intersection (1307)

def Difference.difference_contains source · line 292 · raw

@+xs:List<&2, Bool> -> @+ys:List<&2, Bool> -> @+k:Nat -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, ys) : Nat} -> Type

Difference (1369)

def Difference.difference_mismatch source · line 296 · raw

@+xs:List<&2, Bool> -> @+ys:List<&2, Bool> -> @+h:{Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, ys)) == False{} : Bool} -> Type

Difference (1369)

def Symmetric_Difference.symmetric_difference_contains source · line 300 · raw

@+xs:List<&2, Bool> -> @+ys:List<&2, Bool> -> @+k:Nat -> @+h:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, ys) : Nat} -> Type

Symmetric_Difference (1451)

def Symmetric_Difference.xor_mismatch source · line 304 · raw

@+xs:List<&2, Bool> -> @+ys:List<&2, Bool> -> @+h:{Nat.is_eq(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, xs), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, ys)) == False{} : Bool} -> Type

Symmetric_Difference (1451)

def Elements.to_list_result source · line 308 · raw

@+xs:List<&2, Bool> -> Type

Elements / iteration (Iter_Model)

def Elements.to_list_frame source · line 312 · raw

@+xs:List<&2, Bool> -> Type

Elements / iteration (Iter_Model)

def Elements.elements_contains source · line 316 · raw

@+xs:List<&2, Bool> -> @+k:Nat -> Type

Elements / iteration (Iter_Model)

def Elements.elements_length source · line 320 · raw

@+xs:List<&2, Bool> -> @+off:Nat -> Type

Elements / iteration (Iter_Model)