~/bend-docscommunity

LAWS.bend open laws/TODOs

raw source on the hub · import 0x4b7f9a0323ec18e3ac8e3a9514a1906d/LAWS.bend as LAWS

2 imports
import Base
import ./lib.bend as T

Laws

law pass_true provedin PROOF.bendsource · line 5 · raw

{0x4b7f9a0323ec18e3ac8e3a9514a1906d/lib.Test.pass == True{} : Bool}

pass is True.

law fail_false provedin PROOF.bendsource · line 9 · raw

{0x4b7f9a0323ec18e3ac8e3a9514a1906d/lib.Test.fail == False{} : Bool}

fail is False.

law check_id provedin PROOF.bendsource · line 13 · raw

@b:Bool -> {0x4b7f9a0323ec18e3ac8e3a9514a1906d/lib.Test.check(b) == b : Bool}

check is the identity on Bool.

law all_nil provedin PROOF.bendsource · line 18 · raw

{0x4b7f9a0323ec18e3ac8e3a9514a1906d/lib.Test.all([]) == True{} : Bool}

all(Nil) is True (vacuous).

law all_true_one provedin PROOF.bendsource · line 22 · raw

{0x4b7f9a0323ec18e3ac8e3a9514a1906d/lib.Test.all([True{}]) == True{} : Bool}

all(True <> Nil) is True.

law all_false_one provedin PROOF.bendsource · line 26 · raw

{0x4b7f9a0323ec18e3ac8e3a9514a1906d/lib.Test.all([False{}]) == False{} : Bool}

all(False <> Nil) is False.

law all_true_true provedin PROOF.bendsource · line 30 · raw

{0x4b7f9a0323ec18e3ac8e3a9514a1906d/lib.Test.all([True{}, True{}]) == True{} : Bool}

all(True <> True <> Nil) is True.

law all_true_false provedin PROOF.bendsource · line 34 · raw

{0x4b7f9a0323ec18e3ac8e3a9514a1906d/lib.Test.all([True{}, False{}]) == False{} : Bool}

all(True <> False <> Nil) is False.

law and_list_all provedin PROOF.bendsource · line 38 · raw

@xs:List<&2, Bool> -> {0x4b7f9a0323ec18e3ac8e3a9514a1906d/lib.Test.and_list(xs) == 0x4b7f9a0323ec18e3ac8e3a9514a1906d/lib.Test.all(xs) : Bool}

and_list is Test.all.

law eq_u32_zero provedin PROOF.bendsource · line 43 · raw

{0x4b7f9a0323ec18e3ac8e3a9514a1906d/lib.Test.eq_u32(0, 0) == True{} : Bool}

eq_u32(0, 0) is True.

law eq_u32_ne provedin PROOF.bendsource · line 47 · raw

{0x4b7f9a0323ec18e3ac8e3a9514a1906d/lib.Test.eq_u32(1, 2) == False{} : Bool}

eq_u32(1, 2) is False.

law eq_bool_tt provedin PROOF.bendsource · line 51 · raw

{0x4b7f9a0323ec18e3ac8e3a9514a1906d/lib.Test.eq_bool(True{}, True{}) == True{} : Bool}

eq_bool(True, True) is True.

law eq_bool_tf provedin PROOF.bendsource · line 55 · raw

{0x4b7f9a0323ec18e3ac8e3a9514a1906d/lib.Test.eq_bool(True{}, False{}) == False{} : Bool}

eq_bool(True, False) is False.

law eq_nat_zero provedin PROOF.bendsource · line 59 · raw

{0x4b7f9a0323ec18e3ac8e3a9514a1906d/lib.Test.eq_nat(0n, 0n) == True{} : Bool}

eq_nat(0, 0) is True.

law eq_string_empty provedin PROOF.bendsource · line 63 · raw

{0x4b7f9a0323ec18e3ac8e3a9514a1906d/lib.Test.eq_string("", "") == True{} : Bool}

eq_string("", "") is True.

law eq_string_ne provedin PROOF.bendsource · line 67 · raw

{0x4b7f9a0323ec18e3ac8e3a9514a1906d/lib.Test.eq_string("a", "b") == False{} : Bool}

eq_string("a", "b") is False.

law suite_nil provedin PROOF.bendsource · line 71 · raw

{0x4b7f9a0323ec18e3ac8e3a9514a1906d/lib.Test.suite([]) == True{} : Bool}

suite(Nil) is True.

law suite_one_pass provedin PROOF.bendsource · line 75 · raw

{0x4b7f9a0323ec18e3ac8e3a9514a1906d/lib.Test.suite([0x4b7f9a0323ec18e3ac8e3a9514a1906d/lib.Case{"ok", True{}}]) == True{} : Bool}

suite of one passing case is True.

law suite_one_fail provedin PROOF.bendsource · line 79 · raw

{0x4b7f9a0323ec18e3ac8e3a9514a1906d/lib.Test.suite([0x4b7f9a0323ec18e3ac8e3a9514a1906d/lib.Case{"bad", False{}}]) == False{} : Bool}

suite of one failing case is False.

law case_ok_payload provedin PROOF.bendsource · line 83 · raw

@n:String -> @b:Bool -> {0x4b7f9a0323ec18e3ac8e3a9514a1906d/lib.Test.case_ok(0x4b7f9a0323ec18e3ac8e3a9514a1906d/lib.Case{n, b}) == b : Bool}

case_ok recovers the Bool payload.

law case_ctor provedin PROOF.bendsource · line 89 · raw

@n:String -> @b:Bool -> {0x4b7f9a0323ec18e3ac8e3a9514a1906d/lib.Test.case(n, b) == 0x4b7f9a0323ec18e3ac8e3a9514a1906d/lib.Case{n, b} : 0x4b7f9a0323ec18e3ac8e3a9514a1906d/lib.Test.Case}

Test.case builds Case{name, ok}.

law all_false_true provedin PROOF.bendsource · line 95 · raw

{0x4b7f9a0323ec18e3ac8e3a9514a1906d/lib.Test.all([False{}, True{}]) == False{} : Bool}

all(False <> True <> Nil) is False.

law all_three_true provedin PROOF.bendsource · line 99 · raw

{0x4b7f9a0323ec18e3ac8e3a9514a1906d/lib.Test.all([True{}, True{}, True{}]) == True{} : Bool}

all of three Trues is True.

law eq_bool_ff provedin PROOF.bendsource · line 103 · raw

{0x4b7f9a0323ec18e3ac8e3a9514a1906d/lib.Test.eq_bool(False{}, False{}) == True{} : Bool}

eq_bool(False, False) is True.

law eq_bool_ft provedin PROOF.bendsource · line 107 · raw

{0x4b7f9a0323ec18e3ac8e3a9514a1906d/lib.Test.eq_bool(False{}, True{}) == False{} : Bool}

eq_bool(False, True) is False.

law eq_nat_one provedin PROOF.bendsource · line 111 · raw

{0x4b7f9a0323ec18e3ac8e3a9514a1906d/lib.Test.eq_nat(1n, 1n) == True{} : Bool}

eq_nat(1, 1) is True.

law eq_nat_ne provedin PROOF.bendsource · line 115 · raw

{0x4b7f9a0323ec18e3ac8e3a9514a1906d/lib.Test.eq_nat(0n, 1n) == False{} : Bool}

eq_nat(0, 1) is False.

law eq_u32_one provedin PROOF.bendsource · line 119 · raw

{0x4b7f9a0323ec18e3ac8e3a9514a1906d/lib.Test.eq_u32(1, 1) == True{} : Bool}

eq_u32(1, 1) is True.

law eq_string_aa provedin PROOF.bendsource · line 123 · raw

{0x4b7f9a0323ec18e3ac8e3a9514a1906d/lib.Test.eq_string("a", "a") == True{} : Bool}

eq_string("a", "a") is True.

law suite_two_pass provedin PROOF.bendsource · line 127 · raw

{0x4b7f9a0323ec18e3ac8e3a9514a1906d/lib.Test.suite([0x4b7f9a0323ec18e3ac8e3a9514a1906d/lib.Case{"a", True{}}, 0x4b7f9a0323ec18e3ac8e3a9514a1906d/lib.Case{"b", True{}}]) == True{} : Bool}

suite of two passing cases is True.

law suite_pass_fail provedin PROOF.bendsource · line 135 · raw

{0x4b7f9a0323ec18e3ac8e3a9514a1906d/lib.Test.suite([0x4b7f9a0323ec18e3ac8e3a9514a1906d/lib.Case{"a", True{}}, 0x4b7f9a0323ec18e3ac8e3a9514a1906d/lib.Case{"b", False{}}]) == False{} : Bool}

suite with a failure is False.

law check_true provedin PROOF.bendsource · line 143 · raw

{0x4b7f9a0323ec18e3ac8e3a9514a1906d/lib.Test.check(True{}) == True{} : Bool}

check on concrete Bools.

law check_false provedin PROOF.bendsource · line 146 · raw

{0x4b7f9a0323ec18e3ac8e3a9514a1906d/lib.Test.check(False{}) == False{} : Bool}

law case_ok_via_case provedin PROOF.bendsource · line 150 · raw

@n:String -> @b:Bool -> {0x4b7f9a0323ec18e3ac8e3a9514a1906d/lib.Test.case_ok(0x4b7f9a0323ec18e3ac8e3a9514a1906d/lib.Test.case(n, b)) == b : Bool}

case_ok ∘ case recovers the Bool.