~/bend-docscommunity

LAWS.bend open laws/TODOs

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

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

Laws

law empty_command_parses provedin PROOF.bendsource · line 4 · raw

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

law lookup_preserves_value provedin PROOF.bendsource · line 7 · raw

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

law absent_option_is_none provedin PROOF.bendsource · line 11 · raw

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

law option_and_argument_names_are_separate provedin PROOF.bendsource · line 15 · raw

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

law required_option_preserves_text provedin PROOF.bendsource · line 19 · raw

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

law repeated_value_uses_last provedin PROOF.bendsource · line 23 · raw

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

law repeatable_option_defaults_empty provedin PROOF.bendsource · line 27 · raw

{0x014d1ec5074b05cc46cbfd40d4033fe1/zhao.parse(0x014d1ec5074b05cc46cbfd40d4033fe1/zhao.repeatable_option(0x014d1ec5074b05cc46cbfd40d4033fe1/zhao.command("tool"), "--include <path>", ""), []) == 0x014d1ec5074b05cc46cbfd40d4033fe1/zhao.Parsed{0x014d1ec5074b05cc46cbfd40d4033fe1/zhao.Invocation{["tool"], [0x014d1ec5074b05cc46cbfd40d4033fe1/zhao.Binding{"include", 0x014d1ec5074b05cc46cbfd40d4033fe1/zhao.Many{[]}}], []}} : 0x014d1ec5074b05cc46cbfd40d4033fe1/zhao.Outcome}

law repeatable_option_preserves_order provedin PROOF.bendsource · line 30 · raw

@+first:String -> @+second:String -> {0x014d1ec5074b05cc46cbfd40d4033fe1/zhao.parse(0x014d1ec5074b05cc46cbfd40d4033fe1/zhao.repeatable_option(0x014d1ec5074b05cc46cbfd40d4033fe1/zhao.command("tool"), "--include <path>", ""), ["--include", first, "--include", second]) == 0x014d1ec5074b05cc46cbfd40d4033fe1/zhao.Parsed{0x014d1ec5074b05cc46cbfd40d4033fe1/zhao.Invocation{["tool"], [0x014d1ec5074b05cc46cbfd40d4033fe1/zhao.Binding{"include", 0x014d1ec5074b05cc46cbfd40d4033fe1/zhao.Many{[first, second]}}], []}} : 0x014d1ec5074b05cc46cbfd40d4033fe1/zhao.Outcome}

law repeatable_option_preserves_attached_empty provedin PROOF.bendsource · line 35 · raw

{0x014d1ec5074b05cc46cbfd40d4033fe1/zhao.parse(0x014d1ec5074b05cc46cbfd40d4033fe1/zhao.repeatable_option(0x014d1ec5074b05cc46cbfd40d4033fe1/zhao.command("tool"), "-i, --include <path>", ""), ["--include=", "-ilast"]) == 0x014d1ec5074b05cc46cbfd40d4033fe1/zhao.Parsed{0x014d1ec5074b05cc46cbfd40d4033fe1/zhao.Invocation{["tool"], [0x014d1ec5074b05cc46cbfd40d4033fe1/zhao.Binding{"include", 0x014d1ec5074b05cc46cbfd40d4033fe1/zhao.Many{["", "last"]}}], []}} : 0x014d1ec5074b05cc46cbfd40d4033fe1/zhao.Outcome}

law repeatable_option_missing_value_is_error provedin PROOF.bendsource · line 38 · raw

{0x014d1ec5074b05cc46cbfd40d4033fe1/zhao.parse(0x014d1ec5074b05cc46cbfd40d4033fe1/zhao.repeatable_option(0x014d1ec5074b05cc46cbfd40d4033fe1/zhao.command("tool"), "--include <path>", ""), ["--include"]) == 0x014d1ec5074b05cc46cbfd40d4033fe1/zhao.Error{"zhao.optionMissingArgument", "option '--include' argument missing"} : 0x014d1ec5074b05cc46cbfd40d4033fe1/zhao.Outcome}

law repeatable_option_requires_value_syntax provedin PROOF.bendsource · line 41 · raw

{0x014d1ec5074b05cc46cbfd40d4033fe1/zhao.parse(0x014d1ec5074b05cc46cbfd40d4033fe1/zhao.repeatable_option(0x014d1ec5074b05cc46cbfd40d4033fe1/zhao.command("tool"), "--include [path]", ""), []) == 0x014d1ec5074b05cc46cbfd40d4033fe1/zhao.Error{"zhao.invalidDefinition", "repeatable options require <value> syntax"} : 0x014d1ec5074b05cc46cbfd40d4033fe1/zhao.Outcome}

law negated_option_defaults_true provedin PROOF.bendsource · line 44 · raw

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

law negated_option_sets_false provedin PROOF.bendsource · line 47 · raw

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

law delimiter_makes_help_literal provedin PROOF.bendsource · line 50 · raw

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

law missing_value_is_error provedin PROOF.bendsource · line 53 · raw

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

law unknown_option_is_error provedin PROOF.bendsource · line 56 · raw

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