~/bend-docscommunity

LAWS.bend open laws/TODOs

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

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

Laws

law normalize_empty provedin PROOF.bendsource · line 4 · raw

{0xbe30b4c12fa21816c2b0e099f42f766e/lib.Path.normalize("") == "" : String}

law normalize_absolute_root provedin PROOF.bendsource · line 7 · raw

{0xbe30b4c12fa21816c2b0e099f42f766e/lib.Path.normalize("///") == "/" : String}

law normalize_collapses_slashes provedin PROOF.bendsource · line 10 · raw

{0xbe30b4c12fa21816c2b0e099f42f766e/lib.Path.normalize("/a//b/") == "/a/b" : String}

law normalize_relative provedin PROOF.bendsource · line 13 · raw

{0xbe30b4c12fa21816c2b0e099f42f766e/lib.Path.normalize("a///b") == "a/b" : String}

law normalize_keeps_dot_components provedin PROOF.bendsource · line 16 · raw

{0xbe30b4c12fa21816c2b0e099f42f766e/lib.Path.normalize("a/./b") == "a/./b" : String}

law is_absolute_root provedin PROOF.bendsource · line 19 · raw

{0xbe30b4c12fa21816c2b0e099f42f766e/lib.Path.is_absolute("/tmp") == True{} : Bool}

law is_absolute_relative provedin PROOF.bendsource · line 22 · raw

{0xbe30b4c12fa21816c2b0e099f42f766e/lib.Path.is_absolute("tmp") == False{} : Bool}

law segments_drop_empty provedin PROOF.bendsource · line 25 · raw

{0xbe30b4c12fa21816c2b0e099f42f766e/lib.Path.segments("/a//b/") == ["a", "b"] : List<&2, String>}

law split_is_segments provedin PROOF.bendsource · line 31 · raw

{0xbe30b4c12fa21816c2b0e099f42f766e/lib.Path.split("a/b") == ["a", "b"] : List<&2, String>}

law join_relative provedin PROOF.bendsource · line 37 · raw

{0xbe30b4c12fa21816c2b0e099f42f766e/lib.Path.join("a", "b") == "a/b" : String}

law join_absolute_second provedin PROOF.bendsource · line 40 · raw

{0xbe30b4c12fa21816c2b0e099f42f766e/lib.Path.join("a", "/b") == "/b" : String}

law join_all_segments provedin PROOF.bendsource · line 43 · raw

{0xbe30b4c12fa21816c2b0e099f42f766e/lib.Path.join_all(["a", "b", "c"]) == "a/b/c" : String}

law basename_nested provedin PROOF.bendsource · line 49 · raw

{0xbe30b4c12fa21816c2b0e099f42f766e/lib.Path.basename("/usr//local/bin/") == "bin" : String}

law basename_root provedin PROOF.bendsource · line 52 · raw

{0xbe30b4c12fa21816c2b0e099f42f766e/lib.Path.basename("/") == "" : String}

law dirname_nested provedin PROOF.bendsource · line 55 · raw

{0xbe30b4c12fa21816c2b0e099f42f766e/lib.Path.dirname("/usr//local/bin/") == "/usr/local" : String}

law dirname_single provedin PROOF.bendsource · line 58 · raw

{0xbe30b4c12fa21816c2b0e099f42f766e/lib.Path.dirname("bin") == "." : String}

law dirname_root provedin PROOF.bendsource · line 61 · raw

{0xbe30b4c12fa21816c2b0e099f42f766e/lib.Path.dirname("/") == "/" : String}

law extension_simple provedin PROOF.bendsource · line 64 · raw

{0xbe30b4c12fa21816c2b0e099f42f766e/lib.Path.extension("archive.tar.gz") == ".gz" : String}

law extension_hidden provedin PROOF.bendsource · line 67 · raw

{0xbe30b4c12fa21816c2b0e099f42f766e/lib.Path.extension(".profile") == "" : String}

law extension_hidden_with_suffix provedin PROOF.bendsource · line 70 · raw

{0xbe30b4c12fa21816c2b0e099f42f766e/lib.Path.extension(".profile.bak") == ".bak" : String}

law extension_none provedin PROOF.bendsource · line 73 · raw

{0xbe30b4c12fa21816c2b0e099f42f766e/lib.Path.extension("README") == "" : String}

law is_absolute_empty provedin PROOF.bendsource · line 76 · raw

{0xbe30b4c12fa21816c2b0e099f42f766e/lib.Path.is_absolute("") == False{} : Bool}

law is_absolute_slash provedin PROOF.bendsource · line 79 · raw

{0xbe30b4c12fa21816c2b0e099f42f766e/lib.Path.is_absolute("/") == True{} : Bool}

law segments_empty provedin PROOF.bendsource · line 82 · raw

{0xbe30b4c12fa21816c2b0e099f42f766e/lib.Path.segments("") == [] : List<&2, String>}

law segments_single provedin PROOF.bendsource · line 85 · raw

{0xbe30b4c12fa21816c2b0e099f42f766e/lib.Path.segments("foo") == ["foo"] : List<&2, String>}

law join_empty_empty provedin PROOF.bendsource · line 88 · raw

{0xbe30b4c12fa21816c2b0e099f42f766e/lib.Path.join("", "") == "" : String}

law join_empty_rel provedin PROOF.bendsource · line 91 · raw

{0xbe30b4c12fa21816c2b0e099f42f766e/lib.Path.join("", "a/b") == "a/b" : String}

law join_all_nil provedin PROOF.bendsource · line 94 · raw

{0xbe30b4c12fa21816c2b0e099f42f766e/lib.Path.join_all([]) == "" : String}

law join_all_one provedin PROOF.bendsource · line 97 · raw

{0xbe30b4c12fa21816c2b0e099f42f766e/lib.Path.join_all(["a"]) == "a" : String}

law normalize_idempotent_simple provedin PROOF.bendsource · line 100 · raw

{0xbe30b4c12fa21816c2b0e099f42f766e/lib.Path.normalize(0xbe30b4c12fa21816c2b0e099f42f766e/lib.Path.normalize("/a//b/")) == "/a/b" : String}

law basename_file provedin PROOF.bendsource · line 103 · raw

{0xbe30b4c12fa21816c2b0e099f42f766e/lib.Path.basename("dir/file.txt") == "file.txt" : String}

law dirname_file provedin PROOF.bendsource · line 106 · raw

{0xbe30b4c12fa21816c2b0e099f42f766e/lib.Path.dirname("dir/file.txt") == "dir" : String}

law extension_txt provedin PROOF.bendsource · line 109 · raw

{0xbe30b4c12fa21816c2b0e099f42f766e/lib.Path.extension("file.txt") == ".txt" : String}

law split_eq_segments_abs provedin PROOF.bendsource · line 112 · raw

{0xbe30b4c12fa21816c2b0e099f42f766e/lib.Path.split("/a/b") == 0xbe30b4c12fa21816c2b0e099f42f766e/lib.Path.segments("/a/b") : List<&2, String>}