LAWS.bend source
LAWS.bend on the hub · documented module
import Baseimport ./lib.bend as T# empty is Leaf.law empty_is_leaf: for -a: Quant for -A: Kind(a) { T.Tree.empty(a, A) == T.Leaf{} : T.Tree<a, A> }# leaf is Leaf.law leaf_is_leaf: for -a: Quant for -A: Kind(a) { T.Tree.leaf(a, A) == T.Leaf{} : T.Tree<a, A> }# leaf equals empty.law leaf_eq_empty: for -a: Quant for -A: Kind(a) { T.Tree.leaf(a, A) == T.Tree.empty(a, A) : T.Tree<a, A> }# singleton is Node{Leaf, x, Leaf}.law singleton_is_node: for -a: Quant for -A: Kind(a) for x: A { T.Tree.singleton(a, A, x) == T.Node{T.Leaf{}, x, T.Leaf{}} : T.Tree<a, A> }# size(empty) is 0.law size_empty: for -a: Quant for -A: Kind(a) { T.Tree.size(a, A, T.Tree.empty(a, A)) == 0n : Nat }# size(Leaf) is 0.law size_leaf: for -a: Quant for -A: Kind(a) { T.Tree.size(a, A, T.Leaf{}) == 0n : Nat }# size(singleton(x)) is 1.law size_singleton: for -a: Quant for -A: Kind(a) for x: A { T.Tree.size(a, A, T.Tree.singleton(a, A, x)) == 1n : Nat }# size(Node{Leaf,x,Leaf}) is 1.law size_node_leaves: for -a: Quant for -A: Kind(a) for x: A { T.Tree.size(a, A, T.Node{T.Leaf{}, x, T.Leaf{}}) == 1n : Nat }# Definitional size of Node.law size_node_def: for -a: Quant for -A: Kind(a) for l: T.Tree<a, A> for v: A for r: T.Tree<a, A> { T.Tree.size(a, A, T.Node{l, v, r}) == 1n+Nat.add(T.Tree.size(a, A, l), T.Tree.size(a, A, r)) : Nat }# size(Node{Leaf, x, singleton(y)}) is 2.law size_left_leaf_right_one: for -a: Quant for -A: Kind(a) for x: A for y: A { T.Tree.size(a, A, T.Node{T.Leaf{}, x, T.Tree.singleton(a, A, y)}) == 2n : Nat }# size of balanced three-node tree is 3.law size_both_singletons: for -a: Quant for -A: Kind(a) for x: A for y: A for z: A { T.Tree.size(a, A, T.Node{T.Tree.singleton(a, A, x), y, T.Tree.singleton(a, A, z)}) == 3n : Nat }# to_list(empty) is Nil.law to_list_empty: for -a: Quant for -A: Kind(a) { T.Tree.to_list(a, A, T.Tree.empty(a, A)) == Nil{} : List<a, A> }# to_list(Leaf) is Nil.law to_list_leaf: for -a: Quant for -A: Kind(a) { T.Tree.to_list(a, A, T.Leaf{}) == Nil{} : List<a, A> }# to_list(singleton(x)) is x <> Nil.law to_list_singleton: for -a: Quant for -A: Kind(a) for x: A { T.Tree.to_list(a, A, T.Tree.singleton(a, A, x)) == x <> Nil{} : List<a, A> }# to_list(Node{Leaf,x,Leaf}) is x <> Nil.law to_list_node_leaves: for -a: Quant for -A: Kind(a) for x: A { T.Tree.to_list(a, A, T.Node{T.Leaf{}, x, T.Leaf{}}) == x <> Nil{} : List<a, A> }# to_list with right singleton.law to_list_right_one: for -a: Quant for -A: Kind(a) for x: A for y: A { T.Tree.to_list(a, A, T.Node{T.Leaf{}, x, T.Tree.singleton(a, A, y)}) == x <> (y <> Nil{}) : List<a, A> }# to_list with left singleton.law to_list_left_one: for -a: Quant for -A: Kind(a) for x: A for y: A { T.Tree.to_list(a, A, T.Node{T.Tree.singleton(a, A, x), y, T.Leaf{}}) == x <> (y <> Nil{}) : List<a, A> }# is_empty(empty) is True.law is_empty_empty: for -a: Quant for -A: Kind(a) { T.Tree.is_empty(a, A, T.Tree.empty(a, A)) == True{} : Bool }# is_empty(Leaf) is True.law is_empty_leaf: for -a: Quant for -A: Kind(a) { T.Tree.is_empty(a, A, T.Leaf{}) == True{} : Bool }# is_empty(singleton(x)) is False.law is_empty_singleton: for -a: Quant for -A: Kind(a) for x: A { T.Tree.is_empty(a, A, T.Tree.singleton(a, A, x)) == False{} : Bool }# is_empty(Node{...}) is False.law is_empty_node: for -a: Quant for -A: Kind(a) for l: T.Tree<a, A> for v: A for r: T.Tree<a, A> { T.Tree.is_empty(a, A, T.Node{l, v, r}) == False{} : Bool }