~/bend-docscommunity

LAWS.bend open laws/TODOs

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

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

Laws

law parse_roundtrip_zero provedin PROOF.bendsource · line 5 · raw

{0x697f24d2ad7ac8b3f8c00016670be6af/lib.Semver.parse(0x697f24d2ad7ac8b3f8c00016670be6af/lib.Semver.show(0x697f24d2ad7ac8b3f8c00016670be6af/lib.Semver{0, 0, 0})) == Some{0x697f24d2ad7ac8b3f8c00016670be6af/lib.Semver{0, 0, 0}} : Maybe<&2, 0x697f24d2ad7ac8b3f8c00016670be6af/lib.Semver>}

Concrete parse/show roundtrips for representative versions.

law parse_roundtrip_small provedin PROOF.bendsource · line 9 · raw

{0x697f24d2ad7ac8b3f8c00016670be6af/lib.Semver.parse(0x697f24d2ad7ac8b3f8c00016670be6af/lib.Semver.show(0x697f24d2ad7ac8b3f8c00016670be6af/lib.Semver{1, 2, 3})) == Some{0x697f24d2ad7ac8b3f8c00016670be6af/lib.Semver{1, 2, 3}} : Maybe<&2, 0x697f24d2ad7ac8b3f8c00016670be6af/lib.Semver>}

law parse_roundtrip_large provedin PROOF.bendsource · line 13 · raw

{0x697f24d2ad7ac8b3f8c00016670be6af/lib.Semver.parse(0x697f24d2ad7ac8b3f8c00016670be6af/lib.Semver.show(0x697f24d2ad7ac8b3f8c00016670be6af/lib.Semver{4294967295, 17, 0})) == Some{0x697f24d2ad7ac8b3f8c00016670be6af/lib.Semver{4294967295, 17, 0}} : Maybe<&2, 0x697f24d2ad7ac8b3f8c00016670be6af/lib.Semver>}

law parse_literal provedin PROOF.bendsource · line 17 · raw

{0x697f24d2ad7ac8b3f8c00016670be6af/lib.Semver.parse("12.34.56") == Some{0x697f24d2ad7ac8b3f8c00016670be6af/lib.Semver{12, 34, 56}} : Maybe<&2, 0x697f24d2ad7ac8b3f8c00016670be6af/lib.Semver>}

law parse_reject_missing_component provedin PROOF.bendsource · line 21 · raw

{0x697f24d2ad7ac8b3f8c00016670be6af/lib.Semver.parse("1.2") == None{} : Maybe<&2, 0x697f24d2ad7ac8b3f8c00016670be6af/lib.Semver>}

law parse_reject_metadata provedin PROOF.bendsource · line 24 · raw

{0x697f24d2ad7ac8b3f8c00016670be6af/lib.Semver.parse("1.2.3-alpha") == None{} : Maybe<&2, 0x697f24d2ad7ac8b3f8c00016670be6af/lib.Semver>}

law parse_reject_extra_component provedin PROOF.bendsource · line 27 · raw

{0x697f24d2ad7ac8b3f8c00016670be6af/lib.Semver.parse("1.2.3.4") == None{} : Maybe<&2, 0x697f24d2ad7ac8b3f8c00016670be6af/lib.Semver>}

law cmp_major_lt provedin PROOF.bendsource · line 31 · raw

{0x697f24d2ad7ac8b3f8c00016670be6af/lib.Semver.cmp(0x697f24d2ad7ac8b3f8c00016670be6af/lib.Semver{1, 0, 0}, 0x697f24d2ad7ac8b3f8c00016670be6af/lib.Semver{2, 0, 0}) == LT{} : Cmp}

Numeric precedence cases: major, minor, patch, and equality.

law cmp_minor_lt provedin PROOF.bendsource · line 34 · raw

{0x697f24d2ad7ac8b3f8c00016670be6af/lib.Semver.cmp(0x697f24d2ad7ac8b3f8c00016670be6af/lib.Semver{1, 1, 9}, 0x697f24d2ad7ac8b3f8c00016670be6af/lib.Semver{1, 2, 0}) == LT{} : Cmp}

law cmp_patch_lt provedin PROOF.bendsource · line 37 · raw

{0x697f24d2ad7ac8b3f8c00016670be6af/lib.Semver.cmp(0x697f24d2ad7ac8b3f8c00016670be6af/lib.Semver{1, 2, 3}, 0x697f24d2ad7ac8b3f8c00016670be6af/lib.Semver{1, 2, 4}) == LT{} : Cmp}

law cmp_eq provedin PROOF.bendsource · line 40 · raw

{0x697f24d2ad7ac8b3f8c00016670be6af/lib.Semver.cmp(0x697f24d2ad7ac8b3f8c00016670be6af/lib.Semver{7, 8, 9}, 0x697f24d2ad7ac8b3f8c00016670be6af/lib.Semver{7, 8, 9}) == EQ{} : Cmp}

law cmp_gt provedin PROOF.bendsource · line 43 · raw

{0x697f24d2ad7ac8b3f8c00016670be6af/lib.Semver.cmp(0x697f24d2ad7ac8b3f8c00016670be6af/lib.Semver{2, 0, 0}, 0x697f24d2ad7ac8b3f8c00016670be6af/lib.Semver{1, 99, 99}) == GT{} : Cmp}

law precedes_true provedin PROOF.bendsource · line 46 · raw

{0x697f24d2ad7ac8b3f8c00016670be6af/lib.Semver.precedes(0x697f24d2ad7ac8b3f8c00016670be6af/lib.Semver{1, 2, 3}, 0x697f24d2ad7ac8b3f8c00016670be6af/lib.Semver{1, 2, 4}) == True{} : Bool}

law precedes_false_on_equal provedin PROOF.bendsource · line 49 · raw

{0x697f24d2ad7ac8b3f8c00016670be6af/lib.Semver.precedes(0x697f24d2ad7ac8b3f8c00016670be6af/lib.Semver{1, 2, 3}, 0x697f24d2ad7ac8b3f8c00016670be6af/lib.Semver{1, 2, 3}) == False{} : Bool}