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 sentenceA
. 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 sentenceA
. The output is unverified.If the argument sentence is of the form
A -> B
, then the output is the sentenceA
. The output is unverified.If the argument sentence is of the form
A <-> B
, then the output is the sentenceB -> 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)