LAWS.bend source

LAWS.bend on the hub · documented module

import Baseimport ./lib.bend as T# pass is True.law pass_true:  { T.Test.pass() == True{} : Bool }# fail is False.law fail_false:  { T.Test.fail() == False{} : Bool }# check is the identity on Bool.law check_id:  for b: Bool  { T.Test.check(b) == b : Bool }# all(Nil) is True (vacuous).law all_nil:  { T.Test.all(Nil{}) == True{} : Bool }# all(True <> Nil) is True.law all_true_one:  { T.Test.all(True{} <> Nil{}) == True{} : Bool }# all(False <> Nil) is False.law all_false_one:  { T.Test.all(False{} <> Nil{}) == False{} : Bool }# all(True <> True <> Nil) is True.law all_true_true:  { T.Test.all(True{} <> True{} <> Nil{}) == True{} : Bool }# all(True <> False <> Nil) is False.law all_true_false:  { T.Test.all(True{} <> False{} <> Nil{}) == False{} : Bool }# and_list is Test.all.law and_list_all:  for xs: List<&2, Bool>  { T.Test.and_list(xs) == T.Test.all(xs) : Bool }# eq_u32(0, 0) is True.law eq_u32_zero:  { T.Test.eq_u32(0, 0) == True{} : Bool }# eq_u32(1, 2) is False.law eq_u32_ne:  { T.Test.eq_u32(1, 2) == False{} : Bool }# eq_bool(True, True) is True.law eq_bool_tt:  { T.Test.eq_bool(True{}, True{}) == True{} : Bool }# eq_bool(True, False) is False.law eq_bool_tf:  { T.Test.eq_bool(True{}, False{}) == False{} : Bool }# eq_nat(0, 0) is True.law eq_nat_zero:  { T.Test.eq_nat(0n, 0n) == True{} : Bool }# eq_string("", "") is True.law eq_string_empty:  { T.Test.eq_string("", "") == True{} : Bool }# eq_string("a", "b") is False.law eq_string_ne:  { T.Test.eq_string("a", "b") == False{} : Bool }# suite(Nil) is True.law suite_nil:  { T.Test.suite(Nil{}) == True{} : Bool }# suite of one passing case is True.law suite_one_pass:  { T.Test.suite(T.Case{"ok", True{}} <> Nil{}) == True{} : Bool }# suite of one failing case is False.law suite_one_fail:  { T.Test.suite(T.Case{"bad", False{}} <> Nil{}) == False{} : Bool }# case_ok recovers the Bool payload.law case_ok_payload:  for n: String  for b: Bool  { T.Test.case_ok(T.Case{n, b}) == b : Bool }# Test.case builds Case{name, ok}.law case_ctor:  for n: String  for b: Bool  { T.Test.case(n, b) == T.Case{n, b} : T.Test.Case }# all(False <> True <> Nil) is False.law all_false_true:  { T.Test.all(False{} <> True{} <> Nil{}) == False{} : Bool }# all of three Trues is True.law all_three_true:  { T.Test.all(True{} <> True{} <> True{} <> Nil{}) == True{} : Bool }# eq_bool(False, False) is True.law eq_bool_ff:  { T.Test.eq_bool(False{}, False{}) == True{} : Bool }# eq_bool(False, True) is False.law eq_bool_ft:  { T.Test.eq_bool(False{}, True{}) == False{} : Bool }# eq_nat(1, 1) is True.law eq_nat_one:  { T.Test.eq_nat(1n, 1n) == True{} : Bool }# eq_nat(0, 1) is False.law eq_nat_ne:  { T.Test.eq_nat(0n, 1n) == False{} : Bool }# eq_u32(1, 1) is True.law eq_u32_one:  { T.Test.eq_u32(1, 1) == True{} : Bool }# eq_string("a", "a") is True.law eq_string_aa:  { T.Test.eq_string("a", "a") == True{} : Bool }# suite of two passing cases is True.law suite_two_pass:  {    T.Test.suite(T.Case{"a", True{}} <> T.Case{"b", True{}} <> Nil{})      == True{}    : Bool  }# suite with a failure is False.law suite_pass_fail:  {    T.Test.suite(T.Case{"a", True{}} <> T.Case{"b", False{}} <> Nil{})      == False{}    : Bool  }# check on concrete Bools.law check_true:  { T.Test.check(True{}) == True{} : Bool }law check_false:  { T.Test.check(False{}) == False{} : Bool }# case_ok ∘ case recovers the Bool.law case_ok_via_case:  for n: String  for b: Bool  { T.Test.case_ok(T.Test.case(n, b)) == b : Bool }