~/bend-docscommunity

LAWS.bend open laws/TODOs

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

2 imports
import Base
import ./zhao.bend as Zhao

Laws

law empty_command_parses provedin PROOF.bendsource · line 4 · raw

{0xce17616509f7a12021b2ba6618bac110/zhao.parse(0xce17616509f7a12021b2ba6618bac110/zhao.command("tool"), []) == 0xce17616509f7a12021b2ba6618bac110/zhao.Parsed{0xce17616509f7a12021b2ba6618bac110/zhao.Invocation{["tool"], [], []}} : 0xce17616509f7a12021b2ba6618bac110/zhao.Outcome}

law lookup_preserves_value provedin PROOF.bendsource · line 7 · raw

@+value:0xce17616509f7a12021b2ba6618bac110/zhao.Value -> {0xce17616509f7a12021b2ba6618bac110/zhao.get(0xce17616509f7a12021b2ba6618bac110/zhao.Invocation{[], [0xce17616509f7a12021b2ba6618bac110/zhao.Binding{"key", value}], []}, "key") == Some{value} : Maybe<&2, 0xce17616509f7a12021b2ba6618bac110/zhao.Value>}

law absent_option_is_none provedin PROOF.bendsource · line 11 · raw

@key:String -> {0xce17616509f7a12021b2ba6618bac110/zhao.get(0xce17616509f7a12021b2ba6618bac110/zhao.Invocation{[], [], []}, key) == None{} : Maybe<&2, 0xce17616509f7a12021b2ba6618bac110/zhao.Value>}

law option_and_argument_names_are_separate provedin PROOF.bendsource · line 15 · raw

@value:0xce17616509f7a12021b2ba6618bac110/zhao.Value -> {0xce17616509f7a12021b2ba6618bac110/zhao.get(0xce17616509f7a12021b2ba6618bac110/zhao.Invocation{[], [], [0xce17616509f7a12021b2ba6618bac110/zhao.Binding{"name", value}]}, "name") == None{} : Maybe<&2, 0xce17616509f7a12021b2ba6618bac110/zhao.Value>}

law required_option_preserves_text provedin PROOF.bendsource · line 19 · raw

@+text:String -> {0xce17616509f7a12021b2ba6618bac110/zhao.parse(0xce17616509f7a12021b2ba6618bac110/zhao.option(0xce17616509f7a12021b2ba6618bac110/zhao.command("tool"), "--label <value>", ""), ["--label", text]) == 0xce17616509f7a12021b2ba6618bac110/zhao.Parsed{0xce17616509f7a12021b2ba6618bac110/zhao.Invocation{["tool"], [0xce17616509f7a12021b2ba6618bac110/zhao.Binding{"label", 0xce17616509f7a12021b2ba6618bac110/zhao.Text{text}}], []}} : 0xce17616509f7a12021b2ba6618bac110/zhao.Outcome}

law repeated_value_uses_last provedin PROOF.bendsource · line 23 · raw

@+text:String -> {0xce17616509f7a12021b2ba6618bac110/zhao.parse(0xce17616509f7a12021b2ba6618bac110/zhao.option(0xce17616509f7a12021b2ba6618bac110/zhao.command("tool"), "--label <value>", ""), ["--label=first", "--label", text]) == 0xce17616509f7a12021b2ba6618bac110/zhao.Parsed{0xce17616509f7a12021b2ba6618bac110/zhao.Invocation{["tool"], [0xce17616509f7a12021b2ba6618bac110/zhao.Binding{"label", 0xce17616509f7a12021b2ba6618bac110/zhao.Text{text}}], []}} : 0xce17616509f7a12021b2ba6618bac110/zhao.Outcome}

law negated_option_defaults_true provedin PROOF.bendsource · line 27 · raw

{0xce17616509f7a12021b2ba6618bac110/zhao.parse(0xce17616509f7a12021b2ba6618bac110/zhao.option(0xce17616509f7a12021b2ba6618bac110/zhao.command("tool"), "--no-color", ""), []) == 0xce17616509f7a12021b2ba6618bac110/zhao.Parsed{0xce17616509f7a12021b2ba6618bac110/zhao.Invocation{["tool"], [0xce17616509f7a12021b2ba6618bac110/zhao.Binding{"color", 0xce17616509f7a12021b2ba6618bac110/zhao.Boolean{True{}}}], []}} : 0xce17616509f7a12021b2ba6618bac110/zhao.Outcome}

law negated_option_sets_false provedin PROOF.bendsource · line 30 · raw

{0xce17616509f7a12021b2ba6618bac110/zhao.parse(0xce17616509f7a12021b2ba6618bac110/zhao.option(0xce17616509f7a12021b2ba6618bac110/zhao.command("tool"), "--no-color", ""), ["--no-color"]) == 0xce17616509f7a12021b2ba6618bac110/zhao.Parsed{0xce17616509f7a12021b2ba6618bac110/zhao.Invocation{["tool"], [0xce17616509f7a12021b2ba6618bac110/zhao.Binding{"color", 0xce17616509f7a12021b2ba6618bac110/zhao.Boolean{False{}}}], []}} : 0xce17616509f7a12021b2ba6618bac110/zhao.Outcome}

law delimiter_makes_help_literal provedin PROOF.bendsource · line 33 · raw

{0xce17616509f7a12021b2ba6618bac110/zhao.parse(0xce17616509f7a12021b2ba6618bac110/zhao.argument(0xce17616509f7a12021b2ba6618bac110/zhao.command("tool"), "<name>", ""), ["--", "--help"]) == 0xce17616509f7a12021b2ba6618bac110/zhao.Parsed{0xce17616509f7a12021b2ba6618bac110/zhao.Invocation{["tool"], [], [0xce17616509f7a12021b2ba6618bac110/zhao.Binding{"name", 0xce17616509f7a12021b2ba6618bac110/zhao.Text{"--help"}}]}} : 0xce17616509f7a12021b2ba6618bac110/zhao.Outcome}

law missing_value_is_error provedin PROOF.bendsource · line 36 · raw

{0xce17616509f7a12021b2ba6618bac110/zhao.parse(0xce17616509f7a12021b2ba6618bac110/zhao.option(0xce17616509f7a12021b2ba6618bac110/zhao.command("tool"), "--label <value>", ""), ["--label"]) == 0xce17616509f7a12021b2ba6618bac110/zhao.Error{"zhao.optionMissingArgument", "option '--label' argument missing"} : 0xce17616509f7a12021b2ba6618bac110/zhao.Outcome}

law unknown_option_is_error provedin PROOF.bendsource · line 39 · raw

{0xce17616509f7a12021b2ba6618bac110/zhao.parse(0xce17616509f7a12021b2ba6618bac110/zhao.command("tool"), ["--unknown"]) == 0xce17616509f7a12021b2ba6618bac110/zhao.Error{"zhao.unknownOption", "unknown option '--unknown'"} : 0xce17616509f7a12021b2ba6618bac110/zhao.Outcome}