CORE-verifier
latest
  • Install
  • Predicate Logic
  • Expressions
    • Expression Values
    • Variables
    • Object Substitution
    • Pipe Operator
    • Deduction
    • Sentence Constants
    • Predicate Definitions
    • Expression Brackets
    • Built-in Functions
      • left
      • right
      • and
      • or
      • iff
      • trivial
      • expand
      • substitute
      • branch
  • Commands
CORE-verifier
  • Expressions
  • Built-in Functions
  • right
  • Edit on GitHub

right

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

Syntax

right([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 B. 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 B. The output is unverified.

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

  • If the argument sentence is of the form A <-> B, then the output is the sentence A -> B. 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:

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

Is the unverified sentence:

Y < X

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:

right(test)

Is the verified sentence:

~X in X
Previous Next

© Copyright 2023. Revision 7b0f5dee.

Built with Sphinx using a theme provided by Read the Docs.