left

The built-in function left accepts one sentence expression value and returns the left-hand side of the sentence. It’s precise behavior depends on the input value.

Syntax

left([sentence argument expression])

Behavior

If the argument does not evaluate to a sentence expression value or the argument sentence has unbound objects or propositions, an error is raised.

The following lists the behavior of the function depending on the argument sentence type:

  • If the argument sentence is of the form A & B, then the output is the sentence A. The output is verified if and only if the argument sentence is verified.

  • If the argument sentence is of the form A | B, then the output is the sentence A. The output is unverified.

  • If the argument sentence is of the form A -> B, then the output is the sentence A. The output is unverified.

  • If the argument sentence is of the form A <-> B, then the output is the sentence B -> A. The output is verified if and only if the argument sentence is verified.

  • If the argument sentence is not any of these types, an error is raised

Note

Since this function’s output depends on the association of the operations composing the argument sentence which normally doesn’t matter, this function’s use is not recommended. Oftentimes this function’s purpose is overshadowed by trivial implication and variable assignment.

Examples

If X and Y are objects, < is a relation, the output of the following expression:

left(<: X < Y & Y < X>)

Is the unverified sentence:

X < Y

If X is an object, empty is a definition, in is a relation, and test stores the verified sentence:

^E(empty(E) & E in X) & ~X in X

Then the output of the following expression:

left(test)

Is the verified sentence:

^E(empty(E) & E in X)