set.bend checks

raw source on the hub · import 0x4c3090ea8722081700f9d99ea7503e43/set.bend as MSet

1 import

import Base

Laws

law set_mem_hit provedsource · line 119 · raw

{smember(sinsert(sempty, 5), 5) == (US{[5]}, True{}) : Pair(USet, Bool)}

law set_size_two provedsource · line 125 · raw

{ssize(sinsert(sinsert(sempty, 1), 2)) == 2 : U32}

law set_size_dedup provedsource · line 131 · raw

{ssize(sinsert(sinsert(sempty, 1), 1)) == 1 : U32}

law ssize_empty provedsource · line 137 · raw

{ssize(sempty) == 0 : U32}

Types

type USet source · line 12 · raw

Data

US
```
@elems:List<&2, U32> -> USet
```

Definitions

def sempty source · line 15 · raw

USet

def sput source · line 21 · raw

@lt:Bool -> @eq:Bool -> @x:U32 -> @h:U32 -> @t:List<&2, U32> -> @r:List<&2, U32> -> List<&2, U32>

sput: insert-branch. lt/eq compare x against head h; t is the original tail, r the recursively-inserted tail. x<h -> x<>h<>t (drop r); x==h -> h<>t (drop r, dedup); else h<>r (drop t).

def sinsert_go source · line 30 · raw

@xs:List<&2, U32> -> @+x:U32 -> List<&2, U32>

def sinsert source · line 37 · raw

@s:USet -> @+x:U32 -> USet

def smem_list source · line 42 · raw

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

def smem_b source · line 49 · raw

@+s:USet -> @+x:U32 -> Bool

def smember source · line 54 · raw

@+s:USet -> @+x:U32 -> Pair(USet, Bool)

def sunion_go source · line 57 · raw

@ys:List<&2, U32> -> @acc:USet -> USet

def sunion source · line 64 · raw

@+a:USet -> @+b:USet -> USet

def sinter_put source · line 69 · raw

@keep:Bool -> @h:U32 -> @r:List<&2, U32> -> List<&2, U32>

def sinter_go source · line 76 · raw

@xs:List<&2, U32> -> @+b:USet -> List<&2, U32>

def sinter source · line 83 · raw

@a:USet -> @+b:USet -> USet

def sdiff_put source · line 88 · raw

@found:Bool -> @h:U32 -> @r:List<&2, U32> -> List<&2, U32>

def sdiff_go source · line 95 · raw

@xs:List<&2, U32> -> @+b:USet -> List<&2, U32>

def sdiff source · line 102 · raw

@a:USet -> @+b:USet -> USet

def sllen source · line 107 · raw

@xs:List<&2, U32> -> @acc:U32 -> U32

def ssize source · line 114 · raw

@s:USet -> U32