LAWS.bend source

LAWS.bend on the hub · documented module

import Baseimport ./lib.bend as Ulaw empty_find_is_singleton:  { U.UnionFind.find(U.UnionFind.empty(), 7) == 7 : U32 }law new_is_empty:  { U.UnionFind.new() == U.UnionFind.empty() : U.UnionFind }law connected_is_reflexive:  { U.UnionFind.connected(U.UnionFind.empty(), 7, 7) == True{} : Bool }law union_connects_arguments:  {    U.UnionFind.connected(U.UnionFind.union(U.UnionFind.empty(), 7, 11), 7, 11)      == True{}    : Bool  }law union_is_idempotent_for_connection:  {    U.UnionFind.connected(      U.UnionFind.union(U.UnionFind.union(U.UnionFind.empty(), 7, 11), 7, 11),      7, 11    ) == True{}    : Bool  }law union_preserves_root_of_first:  {    U.UnionFind.find(U.UnionFind.union(U.UnionFind.empty(), 7, 11), 7) == 7    : U32  }law union_transitive_chain:  {    U.UnionFind.connected(      U.UnionFind.union(U.UnionFind.union(U.UnionFind.empty(), 1, 2), 2, 3),      1, 3    ) == True{}    : Bool  }