Documenting built-in functions

docs/and.rst

@@ -0,0 +1,57 @@
+and
+===
+
+The built-in function ``and`` accepts one or more :ref:`sentence expression values <sentencevalue>` and returns a sentence which links each argument sentence using the ``&`` :ref:`connective <and>`.
+
+Syntax
+------
+
+.. code-block::
+
+	and([sentence argument expression], ...)
+
+Behavior
+--------
+
+``and`` accepts one or more argument expressions. If any argument expression does not evaluate to a :ref:`sentence expression value <sentencevalue>` or any argument sentence has unbound objects or predicates, then an error is raised. Otherwise, the output is a sentence composed of each argument sentence joined in order using the ``&`` :ref:`connective <and>`.
+
+The output sentence value is verified if every argument sentence value is verified.
+
+Examples
+--------
+
+If ``in`` is a :doc:`relation <relations>`, ``arg0`` stores the verified sentence:
+
+.. code-block::
+
+	*X*Y(~X in Y | ~Y in X)
+
+And ``arg1`` stores the verified sentence:
+
+.. code-block::
+
+	~^X(X in X)
+
+Then the following expression:
+
+.. code-block::
+
+	and(arg0, arg1)
+
+Evaluates to the following verified sentence:
+
+.. code-block::
+
+	*X*Y(~X in Y | ~Y in X) & ~^X(X in X)
+
+Additionally, the following expression:
+
+.. code-block::
+
+	and(arg0, <:^X^Y(X in Y & Y in X)>, <:^E*X(~X in E)>)
+
+Evaluates to the following unverified sentence:
+
+.. code-block::
+
+	*X*Y(~X in Y | Y in X) & ^X^Y(X in Y & Y in X) & ^E*X(~X in E)

docs/builtin.rst

@@ -0,0 +1,13 @@
+Built-in Functions
+==================
+
+There are a few built-in functions for manipulating :ref:`expression values <expressionvalues>` in CORE. Each built-in function expression begins with an identifier followed by a ``(`` character. A built-in function expression term evaluates to the output of the function. You can determine the behavior of the built-in functions in the documents below.
+
+.. toctree::
+	:titlesonly:
+
+	left <left>
+	right <right>
+	and <and>
+	or <or>
+

docs/connectives.rst

@@ -28,6 +28,8 @@ The logical connective ``&`` represents "and." If ``{A}`` and ``{B}`` represent
 
 Sentences composed with the ``&`` logical connective can be constructed using the built-in function :doc:`and <andfunc>`. A sentence composed with the ``&`` connective can be deconstructed into its constituent sentences using :doc:`variable assignment <varassign>`. A sentence ``{C}`` is stronger than the sentence ``{A} & {B}`` if ``{C}`` is stronger than both ``{A}`` and ``{B}``. The sentence ``{A} & {B}`` is stronger than a sentence ``{C}`` if either ``{A}`` or ``{B}`` is stonger than ``{C}``. See :ref:`Trivial Implication <trivialimp>` for more information.
 
+.. _or:
+
 Or
 ---
 

docs/expressions.rst

@@ -13,6 +13,7 @@ Expressions allow the programmer to combine expression values to obtain new expr
 	Deduction <deduction>
 	Sentence Constants <sentenceconstants>
 	Expression Brackets <brackets>
+	Built-in Functions <builtin>
 
 .. _`expressionvalues`:
 

docs/left.rst

@@ -0,0 +1,61 @@
+left
+====
+
+The built-in function ``left`` accepts one :ref:`sentence expression value <sentencevalue>` and returns the left-hand side of the sentence. It's precise behavior depends on the input value.
+
+Syntax
+------
+
+.. code-block::
+
+	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 :ref:`trivial implication <trivialimplication>` and :doc:`variable assignment <assign>`.
+
+Examples
+--------
+
+If ``X`` and ``Y`` are objects, ``<`` is a relation, the output of the following expression:
+
+.. code-block::
+
+	left(<: X < Y & Y < X>)
+
+Is the unverified sentence:
+
+.. code-block::
+
+	X < Y
+
+If ``X`` is an object, ``empty`` is a :doc:`definition <define>`, ``in`` is a :doc:`relation <relations>`, and ``test`` stores the verified sentence:
+
+.. code-block::
+
+	^E(empty(E) & E in X) & ~X in X
+
+Then the output of the following expression:
+
+.. code-block::
+
+	left(test)
+
+Is the verified sentence:
+
+.. code-block::
+
+	^E(empty(E) & E in X)
+

docs/or.rst

@@ -0,0 +1,57 @@
+or
+===
+
+The built-in function ``or`` accepts one or more :ref:`sentence expression values <sentencevalue>` and returns a sentence which links each argument sentence using the ``|`` :ref:`connective <or>`.
+
+Syntax
+------
+
+.. code-block::
+
+	or([sentence argument expression], ...)
+
+Behavior
+--------
+
+``or`` accepts one or more argument expressions. If any argument expression does not evaluate to a :ref:`sentence expression value <sentencevalue>` or any argument sentence has unbound objects or predicates, then an error is raised. Otherwise, the output is a sentence composed of each argument sentence joined in order using the ``|`` :ref:`connective <and>`.
+
+The output sentence value is verified if at least one argument sentence value is verified.
+
+Examples
+--------
+
+If ``in`` is a :doc:`relation <relations>`, ``arg0`` stores the verified sentence:
+
+.. code-block::
+
+	*X*Y(~X in Y | ~Y in X)
+
+And ``arg1`` stores the verified sentence:
+
+.. code-block::
+
+	~^X(X in X)
+
+Then the following expression:
+
+.. code-block::
+
+	or(arg0, arg1)
+
+Evaluates to the following verified sentence:
+
+.. code-block::
+
+	*X*Y(~X in Y | ~Y in X) | ~^X(X in X)
+
+Additionally, the following expression:
+
+.. code-block::
+
+	or(arg0, <:^X^Y(X in Y & Y in X)>, <:^E*X(~X in E)>)
+
+Evaluates to the following verified sentence:
+
+.. code-block::
+
+	*X*Y(~X in Y | Y in X) | ^X^Y(X in Y & Y in X) | ^E*X(~X in E)

docs/right.rst

@@ -0,0 +1,61 @@
+right
+=====
+
+The built-in function ``right`` accepts one :ref:`sentence expression value <sentencevalue>` and returns the right-hand side of the sentence. It's precise behavior depends on the input value.
+
+Syntax
+------
+
+.. code-block::
+
+	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 :ref:`trivial implication <trivialimplication>` and :doc:`variable assignment <assign>`.
+
+Examples
+--------
+
+If ``X`` and ``Y`` are objects, ``<`` is a relation, the output of the following expression:
+
+.. code-block::
+
+	right(<: X < Y & Y < X>)
+
+Is the unverified sentence:
+
+.. code-block::
+
+	Y < X
+
+If ``X`` is an object, ``empty`` is a :doc:`definition <define>`, ``in`` is a :doc:`relation <relations>`, and ``test`` stores the verified sentence:
+
+.. code-block::
+
+	^E(empty(E) & E in X) & ~X in X
+
+Then the output of the following expression:
+
+.. code-block::
+
+	right(test)
+
+Is the verified sentence:
+
+.. code-block::
+
+	~X in X
+