And there we are, Markdown stubs for each function.
I hate filenames, Git hates Bullet • symbol, SNAFU. I have no idea how to properly escape gnarly filenames. I don't want to restrict Joy function names (any non-space, non-[] Unicode) so I just did the quick and dirty thing to make filenames.
This commit is contained in:
parent
dc76b4da2e
commit
58e97aa124
|
|
@ -0,0 +1,25 @@
|
||||||
|
------------------------------------------------------------------------
|
||||||
|
|
||||||
|
# &
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
Same as a & b.
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
## Definition
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Derivation
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Source
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
## Discussion
|
||||||
|
|
||||||
|
## Crosslinks
|
||||||
|
|
@ -0,0 +1,32 @@
|
||||||
|
--------------
|
||||||
|
|
||||||
|
&
|
||||||
|
^^^
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
Same as a & b.
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
Definition
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Derivation
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Source
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
Discussion
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
Crosslinks
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
|
@ -0,0 +1,25 @@
|
||||||
|
------------------------------------------------------------------------
|
||||||
|
|
||||||
|
# &&
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
nulco \[nullary \[false\]\] dip branch
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
## Definition
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Derivation
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Source
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
## Discussion
|
||||||
|
|
||||||
|
## Crosslinks
|
||||||
|
|
@ -0,0 +1,32 @@
|
||||||
|
--------------
|
||||||
|
|
||||||
|
&&
|
||||||
|
^^^^
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
nulco [nullary [false]] dip branch
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
Definition
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Derivation
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Source
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
Discussion
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
Crosslinks
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
|
@ -0,0 +1,25 @@
|
||||||
|
------------------------------------------------------------------------
|
||||||
|
|
||||||
|
# \*
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
Same as a \* b.
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
## Definition
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Derivation
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Source
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
## Discussion
|
||||||
|
|
||||||
|
## Crosslinks
|
||||||
|
|
@ -0,0 +1,32 @@
|
||||||
|
--------------
|
||||||
|
|
||||||
|
*
|
||||||
|
^^^
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
Same as a * b.
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
Definition
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Derivation
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Source
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
Discussion
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
Crosslinks
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
|
@ -0,0 +1,25 @@
|
||||||
|
------------------------------------------------------------------------
|
||||||
|
|
||||||
|
# •
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
The identity function.
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
## Definition
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Derivation
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Source
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
## Discussion
|
||||||
|
|
||||||
|
## Crosslinks
|
||||||
|
|
@ -0,0 +1,32 @@
|
||||||
|
--------------
|
||||||
|
|
||||||
|
•
|
||||||
|
^^^
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
The identity function.
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
Definition
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Derivation
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Source
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
Discussion
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
Crosslinks
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
|
@ -0,0 +1,25 @@
|
||||||
|
------------------------------------------------------------------------
|
||||||
|
|
||||||
|
# \^
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
Same as a \^ b.
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
## Definition
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Derivation
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Source
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
## Discussion
|
||||||
|
|
||||||
|
## Crosslinks
|
||||||
|
|
@ -0,0 +1,32 @@
|
||||||
|
--------------
|
||||||
|
|
||||||
|
^
|
||||||
|
^^^
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
Same as a ^ b.
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
Definition
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Derivation
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Source
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
Discussion
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
Crosslinks
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
|
@ -0,0 +1,25 @@
|
||||||
|
------------------------------------------------------------------------
|
||||||
|
|
||||||
|
# =
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
Same as a == b.
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
## Definition
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Derivation
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Source
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
## Discussion
|
||||||
|
|
||||||
|
## Crosslinks
|
||||||
|
|
@ -0,0 +1,32 @@
|
||||||
|
--------------
|
||||||
|
|
||||||
|
=
|
||||||
|
^^^
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
Same as a == b.
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
Definition
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Derivation
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Source
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
Discussion
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
Crosslinks
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
|
@ -0,0 +1,25 @@
|
||||||
|
------------------------------------------------------------------------
|
||||||
|
|
||||||
|
# !=
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
Same as a != b.
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
## Definition
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Derivation
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Source
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
## Discussion
|
||||||
|
|
||||||
|
## Crosslinks
|
||||||
|
|
@ -0,0 +1,32 @@
|
||||||
|
--------------
|
||||||
|
|
||||||
|
!=
|
||||||
|
^^^^
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
Same as a != b.
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
Definition
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Derivation
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Source
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
Discussion
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
Crosslinks
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
|
@ -0,0 +1,25 @@
|
||||||
|
------------------------------------------------------------------------
|
||||||
|
|
||||||
|
!-\^\^\^\^
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
0 \>=
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
# Definition
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
# Derivation
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
# Source
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
# Discussion
|
||||||
|
|
||||||
|
# Crosslinks
|
||||||
|
|
@ -0,0 +1,32 @@
|
||||||
|
--------------
|
||||||
|
|
||||||
|
!-
|
||||||
|
^^^^
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
0 >=
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
Definition
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Derivation
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Source
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
Discussion
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
Crosslinks
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
|
@ -0,0 +1,25 @@
|
||||||
|
------------------------------------------------------------------------
|
||||||
|
|
||||||
|
# \>
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
Same as a \> b.
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
## Definition
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Derivation
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Source
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
## Discussion
|
||||||
|
|
||||||
|
## Crosslinks
|
||||||
|
|
@ -0,0 +1,32 @@
|
||||||
|
--------------
|
||||||
|
|
||||||
|
>
|
||||||
|
^^^
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
Same as a > b.
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
Definition
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Derivation
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Source
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
Discussion
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
Crosslinks
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
|
@ -0,0 +1,25 @@
|
||||||
|
------------------------------------------------------------------------
|
||||||
|
|
||||||
|
# \>=
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
Same as a \>= b.
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
## Definition
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Derivation
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Source
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
## Discussion
|
||||||
|
|
||||||
|
## Crosslinks
|
||||||
|
|
@ -0,0 +1,32 @@
|
||||||
|
--------------
|
||||||
|
|
||||||
|
>=
|
||||||
|
^^^^
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
Same as a >= b.
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
Definition
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Derivation
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Source
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
Discussion
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
Crosslinks
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
|
@ -0,0 +1,25 @@
|
||||||
|
------------------------------------------------------------------------
|
||||||
|
|
||||||
|
# \>\>
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
Same as a \>\> b.
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
## Definition
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Derivation
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Source
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
## Discussion
|
||||||
|
|
||||||
|
## Crosslinks
|
||||||
|
|
@ -0,0 +1,32 @@
|
||||||
|
--------------
|
||||||
|
|
||||||
|
>>
|
||||||
|
^^^^
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
Same as a >> b.
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
Definition
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Derivation
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Source
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
Discussion
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
Crosslinks
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
|
@ -0,0 +1,25 @@
|
||||||
|
------------------------------------------------------------------------
|
||||||
|
|
||||||
|
-\^\^\^
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
Same as a - b.
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
# Definition
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
# Derivation
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
# Source
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
# Discussion
|
||||||
|
|
||||||
|
# Crosslinks
|
||||||
|
|
@ -0,0 +1,32 @@
|
||||||
|
--------------
|
||||||
|
|
||||||
|
-
|
||||||
|
^^^
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
Same as a - b.
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
Definition
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Derivation
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Source
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
Discussion
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
Crosslinks
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
|
@ -0,0 +1,25 @@
|
||||||
|
------------------------------------------------------------------------
|
||||||
|
|
||||||
|
\--\^\^\^\^
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
Decrement TOS.
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
# Definition
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
# Derivation
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
# Source
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
# Discussion
|
||||||
|
|
||||||
|
# Crosslinks
|
||||||
|
|
@ -0,0 +1,32 @@
|
||||||
|
--------------
|
||||||
|
|
||||||
|
--
|
||||||
|
^^^^
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
Decrement TOS.
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
Definition
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Derivation
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Source
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
Discussion
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
Crosslinks
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
|
@ -0,0 +1,25 @@
|
||||||
|
------------------------------------------------------------------------
|
||||||
|
|
||||||
|
# \<
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
Same as a \< b.
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
## Definition
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Derivation
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Source
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
## Discussion
|
||||||
|
|
||||||
|
## Crosslinks
|
||||||
|
|
@ -0,0 +1,32 @@
|
||||||
|
--------------
|
||||||
|
|
||||||
|
<
|
||||||
|
^^^
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
Same as a < b.
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
Definition
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Derivation
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Source
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
Discussion
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
Crosslinks
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
|
@ -0,0 +1,25 @@
|
||||||
|
------------------------------------------------------------------------
|
||||||
|
|
||||||
|
# \<=
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
Same as a \<= b.
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
## Definition
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Derivation
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Source
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
## Discussion
|
||||||
|
|
||||||
|
## Crosslinks
|
||||||
|
|
@ -0,0 +1,32 @@
|
||||||
|
--------------
|
||||||
|
|
||||||
|
<=
|
||||||
|
^^^^
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
Same as a <= b.
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
Definition
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Derivation
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Source
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
Discussion
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
Crosslinks
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
|
@ -0,0 +1,25 @@
|
||||||
|
------------------------------------------------------------------------
|
||||||
|
|
||||||
|
# \<\>
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
Same as a != b.
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
## Definition
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Derivation
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Source
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
## Discussion
|
||||||
|
|
||||||
|
## Crosslinks
|
||||||
|
|
@ -0,0 +1,32 @@
|
||||||
|
--------------
|
||||||
|
|
||||||
|
<>
|
||||||
|
^^^^
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
Same as a != b.
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
Definition
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Derivation
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Source
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
Discussion
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
Crosslinks
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
|
@ -0,0 +1,25 @@
|
||||||
|
------------------------------------------------------------------------
|
||||||
|
|
||||||
|
# \<{}
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
\[\] swap
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
## Definition
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Derivation
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Source
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
## Discussion
|
||||||
|
|
||||||
|
## Crosslinks
|
||||||
|
|
@ -0,0 +1,32 @@
|
||||||
|
--------------
|
||||||
|
|
||||||
|
<{}
|
||||||
|
^^^^^
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
[] swap
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
Definition
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Derivation
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Source
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
Discussion
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
Crosslinks
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
|
@ -0,0 +1,25 @@
|
||||||
|
------------------------------------------------------------------------
|
||||||
|
|
||||||
|
# \<\<
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
Same as a \<\< b.
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
## Definition
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Derivation
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Source
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
## Discussion
|
||||||
|
|
||||||
|
## Crosslinks
|
||||||
|
|
@ -0,0 +1,32 @@
|
||||||
|
--------------
|
||||||
|
|
||||||
|
<<
|
||||||
|
^^^^
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
Same as a << b.
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
Definition
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Derivation
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Source
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
Discussion
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
Crosslinks
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
|
@ -0,0 +1,25 @@
|
||||||
|
------------------------------------------------------------------------
|
||||||
|
|
||||||
|
# \<\<{}
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
\[\] rollup
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
## Definition
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Derivation
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Source
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
## Discussion
|
||||||
|
|
||||||
|
## Crosslinks
|
||||||
|
|
@ -0,0 +1,32 @@
|
||||||
|
--------------
|
||||||
|
|
||||||
|
<<{}
|
||||||
|
^^^^^^
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
[] rollup
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
Definition
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Derivation
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Source
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
Discussion
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
Crosslinks
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
|
@ -0,0 +1,25 @@
|
||||||
|
------------------------------------------------------------------------
|
||||||
|
|
||||||
|
# %
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
Same as a % b.
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
## Definition
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Derivation
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Source
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
## Discussion
|
||||||
|
|
||||||
|
## Crosslinks
|
||||||
|
|
@ -0,0 +1,32 @@
|
||||||
|
--------------
|
||||||
|
|
||||||
|
%
|
||||||
|
^^^
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
Same as a % b.
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
Definition
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Derivation
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Source
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
Discussion
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
Crosslinks
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
|
@ -0,0 +1,25 @@
|
||||||
|
------------------------------------------------------------------------
|
||||||
|
|
||||||
|
# +
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
Same as a + b.
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
## Definition
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Derivation
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Source
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
## Discussion
|
||||||
|
|
||||||
|
## Crosslinks
|
||||||
|
|
@ -0,0 +1,32 @@
|
||||||
|
--------------
|
||||||
|
|
||||||
|
+
|
||||||
|
^^^
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
Same as a + b.
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
Definition
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Derivation
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Source
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
Discussion
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
Crosslinks
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
|
@ -0,0 +1,25 @@
|
||||||
|
------------------------------------------------------------------------
|
||||||
|
|
||||||
|
# ++
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
Increment TOS.
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
## Definition
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Derivation
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Source
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
## Discussion
|
||||||
|
|
||||||
|
## Crosslinks
|
||||||
|
|
@ -0,0 +1,32 @@
|
||||||
|
--------------
|
||||||
|
|
||||||
|
++
|
||||||
|
^^^^
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
Increment TOS.
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
Definition
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Derivation
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Source
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
Discussion
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
Crosslinks
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
|
@ -0,0 +1,25 @@
|
||||||
|
------------------------------------------------------------------------
|
||||||
|
|
||||||
|
# ?
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
dup bool
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
## Definition
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Derivation
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Source
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
## Discussion
|
||||||
|
|
||||||
|
## Crosslinks
|
||||||
|
|
@ -0,0 +1,32 @@
|
||||||
|
--------------
|
||||||
|
|
||||||
|
?
|
||||||
|
^^^
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
dup bool
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
Definition
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Derivation
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Source
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
Discussion
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
Crosslinks
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
|
@ -0,0 +1,25 @@
|
||||||
|
------------------------------------------------------------------------
|
||||||
|
|
||||||
|
# /
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
Same as a // b.
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
## Definition
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Derivation
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Source
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
## Discussion
|
||||||
|
|
||||||
|
## Crosslinks
|
||||||
|
|
@ -0,0 +1,32 @@
|
||||||
|
--------------
|
||||||
|
|
||||||
|
/
|
||||||
|
^^^
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
Same as a // b.
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
Definition
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Derivation
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Source
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
Discussion
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
Crosslinks
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
|
@ -0,0 +1,25 @@
|
||||||
|
------------------------------------------------------------------------
|
||||||
|
|
||||||
|
# //
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
Same as a // b.
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
## Definition
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Derivation
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Source
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
## Discussion
|
||||||
|
|
||||||
|
## Crosslinks
|
||||||
|
|
@ -0,0 +1,32 @@
|
||||||
|
--------------
|
||||||
|
|
||||||
|
//
|
||||||
|
^^^^
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
Same as a // b.
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
Definition
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Derivation
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Source
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
Discussion
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
Crosslinks
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
|
@ -0,0 +1,25 @@
|
||||||
|
------------------------------------------------------------------------
|
||||||
|
|
||||||
|
# /floor
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
Same as a // b.
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
## Definition
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Derivation
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Source
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
## Discussion
|
||||||
|
|
||||||
|
## Crosslinks
|
||||||
|
|
@ -0,0 +1,32 @@
|
||||||
|
--------------
|
||||||
|
|
||||||
|
/floor
|
||||||
|
^^^^^^^^
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
Same as a // b.
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
Definition
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Derivation
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Source
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
Discussion
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
Crosslinks
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
|
@ -0,0 +1,25 @@
|
||||||
|
------------------------------------------------------------------------
|
||||||
|
|
||||||
|
# \|\|
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
nulco \[nullary\] dip \[true\] branch
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
## Definition
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Derivation
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Source
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
## Discussion
|
||||||
|
|
||||||
|
## Crosslinks
|
||||||
|
|
@ -0,0 +1,32 @@
|
||||||
|
--------------
|
||||||
|
|
||||||
|
||
|
||||||
|
^^^^
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
nulco [nullary] dip [true] branch
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
Definition
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Derivation
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Source
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
Discussion
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
Crosslinks
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
|
@ -0,0 +1,25 @@
|
||||||
|
------------------------------------------------------------------------
|
||||||
|
|
||||||
|
# abs
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
Return the absolute value of the argument.
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
## Definition
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Derivation
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Source
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
## Discussion
|
||||||
|
|
||||||
|
## Crosslinks
|
||||||
|
|
@ -0,0 +1,32 @@
|
||||||
|
--------------
|
||||||
|
|
||||||
|
abs
|
||||||
|
^^^^^
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
Return the absolute value of the argument.
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
Definition
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Derivation
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Source
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
Discussion
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
Crosslinks
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
|
@ -0,0 +1,25 @@
|
||||||
|
------------------------------------------------------------------------
|
||||||
|
|
||||||
|
# add
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
Same as a + b.
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
## Definition
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Derivation
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Source
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
## Discussion
|
||||||
|
|
||||||
|
## Crosslinks
|
||||||
|
|
@ -0,0 +1,32 @@
|
||||||
|
--------------
|
||||||
|
|
||||||
|
add
|
||||||
|
^^^^^
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
Same as a + b.
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
Definition
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Derivation
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Source
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
Discussion
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
Crosslinks
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
|
@ -0,0 +1,25 @@
|
||||||
|
------------------------------------------------------------------------
|
||||||
|
|
||||||
|
# anamorphism
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
\[pop \[\]\] swap \[dip swons\] genrec
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
## Definition
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Derivation
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Source
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
## Discussion
|
||||||
|
|
||||||
|
## Crosslinks
|
||||||
|
|
@ -0,0 +1,32 @@
|
||||||
|
--------------
|
||||||
|
|
||||||
|
anamorphism
|
||||||
|
^^^^^^^^^^^^^
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
[pop []] swap [dip swons] genrec
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
Definition
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Derivation
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Source
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
Discussion
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
Crosslinks
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
|
@ -0,0 +1,25 @@
|
||||||
|
------------------------------------------------------------------------
|
||||||
|
|
||||||
|
# and
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
Same as a & b.
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
## Definition
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Derivation
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Source
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
## Discussion
|
||||||
|
|
||||||
|
## Crosslinks
|
||||||
|
|
@ -0,0 +1,32 @@
|
||||||
|
--------------
|
||||||
|
|
||||||
|
and
|
||||||
|
^^^^^
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
Same as a & b.
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
Definition
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Derivation
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Source
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
Discussion
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
Crosslinks
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
|
@ -0,0 +1,30 @@
|
||||||
|
------------------------------------------------------------------------
|
||||||
|
|
||||||
|
# app2
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
Like app1 with two items.
|
||||||
|
|
||||||
|
: ... y x [Q] . app2
|
||||||
|
-----------------------------------
|
||||||
|
... [y ...] [Q] . infra first
|
||||||
|
[x ...] [Q] infra first
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
## Definition
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Derivation
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Source
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
## Discussion
|
||||||
|
|
||||||
|
## Crosslinks
|
||||||
|
|
@ -0,0 +1,40 @@
|
||||||
|
--------------
|
||||||
|
|
||||||
|
app2
|
||||||
|
^^^^^^
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
Like app1 with two items.
|
||||||
|
::
|
||||||
|
|
||||||
|
... y x [Q] . app2
|
||||||
|
-----------------------------------
|
||||||
|
... [y ...] [Q] . infra first
|
||||||
|
[x ...] [Q] infra first
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
Definition
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Derivation
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Source
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
Discussion
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
Crosslinks
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
|
@ -0,0 +1,31 @@
|
||||||
|
------------------------------------------------------------------------
|
||||||
|
|
||||||
|
# app3
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
Like app1 with three items.
|
||||||
|
|
||||||
|
: ... z y x [Q] . app3
|
||||||
|
-----------------------------------
|
||||||
|
... [z ...] [Q] . infra first
|
||||||
|
[y ...] [Q] infra first
|
||||||
|
[x ...] [Q] infra first
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
## Definition
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Derivation
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Source
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
## Discussion
|
||||||
|
|
||||||
|
## Crosslinks
|
||||||
|
|
@ -0,0 +1,41 @@
|
||||||
|
--------------
|
||||||
|
|
||||||
|
app3
|
||||||
|
^^^^^^
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
Like app1 with three items.
|
||||||
|
::
|
||||||
|
|
||||||
|
... z y x [Q] . app3
|
||||||
|
-----------------------------------
|
||||||
|
... [z ...] [Q] . infra first
|
||||||
|
[y ...] [Q] infra first
|
||||||
|
[x ...] [Q] infra first
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
Definition
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Derivation
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Source
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
Discussion
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
Crosslinks
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
|
@ -0,0 +1,25 @@
|
||||||
|
------------------------------------------------------------------------
|
||||||
|
|
||||||
|
# appN
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
\[grabN\] codi map disenstacken
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
## Definition
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Derivation
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Source
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
## Discussion
|
||||||
|
|
||||||
|
## Crosslinks
|
||||||
|
|
@ -0,0 +1,32 @@
|
||||||
|
--------------
|
||||||
|
|
||||||
|
appN
|
||||||
|
^^^^^^
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
[grabN] codi map disenstacken
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
Definition
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Derivation
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Source
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
Discussion
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
Crosslinks
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
|
@ -0,0 +1,32 @@
|
||||||
|
------------------------------------------------------------------------
|
||||||
|
|
||||||
|
# at
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
getitem == drop first
|
||||||
|
|
||||||
|
Expects an integer and a quote on the stack and returns the item at the
|
||||||
|
nth position in the quote counting from 0. :
|
||||||
|
|
||||||
|
[a b c d] 0 getitem
|
||||||
|
-------------------------
|
||||||
|
a
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
## Definition
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Derivation
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Source
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
## Discussion
|
||||||
|
|
||||||
|
## Crosslinks
|
||||||
|
|
@ -0,0 +1,45 @@
|
||||||
|
--------------
|
||||||
|
|
||||||
|
at
|
||||||
|
^^^^
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
|
||||||
|
::
|
||||||
|
|
||||||
|
getitem == drop first
|
||||||
|
|
||||||
|
Expects an integer and a quote on the stack and returns the item at the
|
||||||
|
nth position in the quote counting from 0.
|
||||||
|
::
|
||||||
|
|
||||||
|
[a b c d] 0 getitem
|
||||||
|
-------------------------
|
||||||
|
a
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
Definition
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Derivation
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Source
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
Discussion
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
Crosslinks
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
|
@ -0,0 +1,25 @@
|
||||||
|
------------------------------------------------------------------------
|
||||||
|
|
||||||
|
# average
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
\[sum\] \[size\] cleave /
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
## Definition
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Derivation
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Source
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
## Discussion
|
||||||
|
|
||||||
|
## Crosslinks
|
||||||
|
|
@ -0,0 +1,32 @@
|
||||||
|
--------------
|
||||||
|
|
||||||
|
average
|
||||||
|
^^^^^^^^^
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
[sum] [size] cleave /
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
Definition
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Derivation
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Source
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
Discussion
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
Crosslinks
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
|
@ -0,0 +1,29 @@
|
||||||
|
------------------------------------------------------------------------
|
||||||
|
|
||||||
|
# bool
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
bool(x) -\> bool
|
||||||
|
|
||||||
|
Returns True when the argument x is true, False otherwise. The builtins
|
||||||
|
True and False are the only two instances of the class bool. The class
|
||||||
|
bool is a subclass of the class int, and cannot be subclassed.
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
## Definition
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Derivation
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Source
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
## Discussion
|
||||||
|
|
||||||
|
## Crosslinks
|
||||||
|
|
@ -0,0 +1,36 @@
|
||||||
|
--------------
|
||||||
|
|
||||||
|
bool
|
||||||
|
^^^^^^
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
bool(x) -> bool
|
||||||
|
|
||||||
|
Returns True when the argument x is true, False otherwise.
|
||||||
|
The builtins True and False are the only two instances of the class bool.
|
||||||
|
The class bool is a subclass of the class int, and cannot be subclassed.
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
Definition
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Derivation
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Source
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
Discussion
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
Crosslinks
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
|
@ -0,0 +1,35 @@
|
||||||
|
------------------------------------------------------------------------
|
||||||
|
|
||||||
|
# branch
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
Use a Boolean value to select one of two quoted programs to run.
|
||||||
|
|
||||||
|
branch == roll< choice i
|
||||||
|
|
||||||
|
False [F] [T] branch
|
||||||
|
--------------------------
|
||||||
|
F
|
||||||
|
|
||||||
|
True [F] [T] branch
|
||||||
|
-------------------------
|
||||||
|
T
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
## Definition
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Derivation
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Source
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
## Discussion
|
||||||
|
|
||||||
|
## Crosslinks
|
||||||
|
|
@ -0,0 +1,49 @@
|
||||||
|
--------------
|
||||||
|
|
||||||
|
branch
|
||||||
|
^^^^^^^^
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
|
||||||
|
Use a Boolean value to select one of two quoted programs to run.
|
||||||
|
|
||||||
|
::
|
||||||
|
|
||||||
|
branch == roll< choice i
|
||||||
|
|
||||||
|
::
|
||||||
|
|
||||||
|
False [F] [T] branch
|
||||||
|
--------------------------
|
||||||
|
F
|
||||||
|
|
||||||
|
True [F] [T] branch
|
||||||
|
-------------------------
|
||||||
|
T
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
Definition
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Derivation
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Source
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
Discussion
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
Crosslinks
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
|
@ -0,0 +1,25 @@
|
||||||
|
------------------------------------------------------------------------
|
||||||
|
|
||||||
|
# ccccons
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
ccons ccons
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
## Definition
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Derivation
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Source
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
## Discussion
|
||||||
|
|
||||||
|
## Crosslinks
|
||||||
|
|
@ -0,0 +1,32 @@
|
||||||
|
--------------
|
||||||
|
|
||||||
|
ccccons
|
||||||
|
^^^^^^^^^
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
ccons ccons
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
Definition
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Derivation
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Source
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
Discussion
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
Crosslinks
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
|
@ -0,0 +1,38 @@
|
||||||
|
------------------------------------------------------------------------
|
||||||
|
|
||||||
|
# choice
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
Use a Boolean value to select one of two items. :
|
||||||
|
|
||||||
|
A B false choice
|
||||||
|
----------------------
|
||||||
|
A
|
||||||
|
|
||||||
|
|
||||||
|
A B true choice
|
||||||
|
---------------------
|
||||||
|
B
|
||||||
|
|
||||||
|
Currently Python semantics are used to evaluate the \"truthiness\" of
|
||||||
|
the Boolean value (so empty string, zero, etc. are counted as false,
|
||||||
|
etc.)
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
## Definition
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Derivation
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Source
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
## Discussion
|
||||||
|
|
||||||
|
## Crosslinks
|
||||||
|
|
@ -0,0 +1,47 @@
|
||||||
|
--------------
|
||||||
|
|
||||||
|
choice
|
||||||
|
^^^^^^^^
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
|
||||||
|
Use a Boolean value to select one of two items.
|
||||||
|
::
|
||||||
|
|
||||||
|
A B false choice
|
||||||
|
----------------------
|
||||||
|
A
|
||||||
|
|
||||||
|
|
||||||
|
A B true choice
|
||||||
|
---------------------
|
||||||
|
B
|
||||||
|
|
||||||
|
Currently Python semantics are used to evaluate the "truthiness" of the
|
||||||
|
Boolean value (so empty string, zero, etc. are counted as false, etc.)
|
||||||
|
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
Definition
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Derivation
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Source
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
Discussion
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
Crosslinks
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
|
@ -0,0 +1,30 @@
|
||||||
|
------------------------------------------------------------------------
|
||||||
|
|
||||||
|
# clear
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
Clear everything from the stack.
|
||||||
|
|
||||||
|
: clear == stack [pop stack] loop
|
||||||
|
|
||||||
|
... clear
|
||||||
|
---------------
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
## Definition
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Derivation
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Source
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
## Discussion
|
||||||
|
|
||||||
|
## Crosslinks
|
||||||
|
|
@ -0,0 +1,40 @@
|
||||||
|
--------------
|
||||||
|
|
||||||
|
clear
|
||||||
|
^^^^^^^
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
Clear everything from the stack.
|
||||||
|
::
|
||||||
|
|
||||||
|
clear == stack [pop stack] loop
|
||||||
|
|
||||||
|
... clear
|
||||||
|
---------------
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
Definition
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Derivation
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Source
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
Discussion
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
Crosslinks
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
|
@ -0,0 +1,25 @@
|
||||||
|
------------------------------------------------------------------------
|
||||||
|
|
||||||
|
# cleave
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
fork popdd
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
## Definition
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Derivation
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Source
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
## Discussion
|
||||||
|
|
||||||
|
## Crosslinks
|
||||||
|
|
@ -0,0 +1,32 @@
|
||||||
|
--------------
|
||||||
|
|
||||||
|
cleave
|
||||||
|
^^^^^^^^
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
fork popdd
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
Definition
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Derivation
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Source
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
Discussion
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
Crosslinks
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
|
@ -0,0 +1,25 @@
|
||||||
|
------------------------------------------------------------------------
|
||||||
|
|
||||||
|
# clop
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
cleave popdd
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
## Definition
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Derivation
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Source
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
## Discussion
|
||||||
|
|
||||||
|
## Crosslinks
|
||||||
|
|
@ -0,0 +1,32 @@
|
||||||
|
--------------
|
||||||
|
|
||||||
|
clop
|
||||||
|
^^^^^^
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
cleave popdd
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
Definition
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Derivation
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Source
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
Discussion
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
Crosslinks
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
|
@ -0,0 +1,38 @@
|
||||||
|
------------------------------------------------------------------------
|
||||||
|
|
||||||
|
# cmp
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
cmp takes two values and three quoted programs on the stack and runs one
|
||||||
|
of the three depending on the results of comparing the two values: :
|
||||||
|
|
||||||
|
a b [G] [E] [L] cmp
|
||||||
|
------------------------- a > b
|
||||||
|
G
|
||||||
|
|
||||||
|
a b [G] [E] [L] cmp
|
||||||
|
------------------------- a = b
|
||||||
|
E
|
||||||
|
|
||||||
|
a b [G] [E] [L] cmp
|
||||||
|
------------------------- a < b
|
||||||
|
L
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
## Definition
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Derivation
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Source
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
## Discussion
|
||||||
|
|
||||||
|
## Crosslinks
|
||||||
|
|
@ -0,0 +1,48 @@
|
||||||
|
--------------
|
||||||
|
|
||||||
|
cmp
|
||||||
|
^^^^^
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
|
||||||
|
cmp takes two values and three quoted programs on the stack and runs
|
||||||
|
one of the three depending on the results of comparing the two values:
|
||||||
|
::
|
||||||
|
|
||||||
|
a b [G] [E] [L] cmp
|
||||||
|
------------------------- a > b
|
||||||
|
G
|
||||||
|
|
||||||
|
a b [G] [E] [L] cmp
|
||||||
|
------------------------- a = b
|
||||||
|
E
|
||||||
|
|
||||||
|
a b [G] [E] [L] cmp
|
||||||
|
------------------------- a < b
|
||||||
|
L
|
||||||
|
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
Definition
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Derivation
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Source
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
Discussion
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
Crosslinks
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
|
@ -0,0 +1,25 @@
|
||||||
|
------------------------------------------------------------------------
|
||||||
|
|
||||||
|
# codi
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
cons dip
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
## Definition
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Derivation
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Source
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
## Discussion
|
||||||
|
|
||||||
|
## Crosslinks
|
||||||
|
|
@ -0,0 +1,32 @@
|
||||||
|
--------------
|
||||||
|
|
||||||
|
codi
|
||||||
|
^^^^^^
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
cons dip
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
Definition
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Derivation
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Source
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
Discussion
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
Crosslinks
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
|
@ -0,0 +1,25 @@
|
||||||
|
------------------------------------------------------------------------
|
||||||
|
|
||||||
|
# codireco
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
codi reco
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
## Definition
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Derivation
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Source
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
## Discussion
|
||||||
|
|
||||||
|
## Crosslinks
|
||||||
|
|
@ -0,0 +1,32 @@
|
||||||
|
--------------
|
||||||
|
|
||||||
|
codireco
|
||||||
|
^^^^^^^^^^
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
codi reco
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
Definition
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Derivation
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Source
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
Discussion
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
Crosslinks
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
|
@ -0,0 +1,29 @@
|
||||||
|
------------------------------------------------------------------------
|
||||||
|
|
||||||
|
# concat
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
Concatinate the two lists on the top of the stack. :
|
||||||
|
|
||||||
|
[a b c] [d e f] concat
|
||||||
|
----------------------------
|
||||||
|
[a b c d e f]
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
## Definition
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Derivation
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Source
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
## Discussion
|
||||||
|
|
||||||
|
## Crosslinks
|
||||||
|
|
@ -0,0 +1,40 @@
|
||||||
|
--------------
|
||||||
|
|
||||||
|
concat
|
||||||
|
^^^^^^^^
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
|
||||||
|
Concatinate the two lists on the top of the stack.
|
||||||
|
::
|
||||||
|
|
||||||
|
[a b c] [d e f] concat
|
||||||
|
----------------------------
|
||||||
|
[a b c d e f]
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
Definition
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Derivation
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Source
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
Discussion
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
Crosslinks
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
|
@ -0,0 +1,36 @@
|
||||||
|
------------------------------------------------------------------------
|
||||||
|
|
||||||
|
# cond
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
This combinator works like a case statement. It expects a single quote
|
||||||
|
on the stack that must contain zero or more condition quotes and a
|
||||||
|
default quote. Each condition clause should contain a quoted predicate
|
||||||
|
followed by the function expression to run if that predicate returns
|
||||||
|
true. If no predicates return true the default function runs.
|
||||||
|
|
||||||
|
It works by rewriting into a chain of nested [ifte]{.title-ref}
|
||||||
|
expressions, e.g.:
|
||||||
|
|
||||||
|
[[[B0] T0] [[B1] T1] [D]] cond
|
||||||
|
-----------------------------------------
|
||||||
|
[B0] [T0] [[B1] [T1] [D] ifte] ifte
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
## Definition
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Derivation
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Source
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
## Discussion
|
||||||
|
|
||||||
|
## Crosslinks
|
||||||
|
|
@ -0,0 +1,45 @@
|
||||||
|
--------------
|
||||||
|
|
||||||
|
cond
|
||||||
|
^^^^^^
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
|
||||||
|
This combinator works like a case statement. It expects a single quote
|
||||||
|
on the stack that must contain zero or more condition quotes and a
|
||||||
|
default quote. Each condition clause should contain a quoted predicate
|
||||||
|
followed by the function expression to run if that predicate returns
|
||||||
|
true. If no predicates return true the default function runs.
|
||||||
|
|
||||||
|
It works by rewriting into a chain of nested `ifte` expressions, e.g.::
|
||||||
|
|
||||||
|
[[[B0] T0] [[B1] T1] [D]] cond
|
||||||
|
-----------------------------------------
|
||||||
|
[B0] [T0] [[B1] [T1] [D] ifte] ifte
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
Definition
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Derivation
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Source
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
Discussion
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
Crosslinks
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
|
@ -0,0 +1,25 @@
|
||||||
|
------------------------------------------------------------------------
|
||||||
|
|
||||||
|
# dinfrirst
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
dip infrst
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
## Definition
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Derivation
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Source
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
## Discussion
|
||||||
|
|
||||||
|
## Crosslinks
|
||||||
|
|
@ -0,0 +1,32 @@
|
||||||
|
--------------
|
||||||
|
|
||||||
|
dinfrirst
|
||||||
|
^^^^^^^^^^^
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
dip infrst
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
Definition
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Derivation
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Source
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
Discussion
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
Crosslinks
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
|
@ -0,0 +1,31 @@
|
||||||
|
------------------------------------------------------------------------
|
||||||
|
|
||||||
|
# dip
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
The dip combinator expects a quoted program on the stack and below it
|
||||||
|
some item, it hoists the item into the expression and runs the program
|
||||||
|
on the rest of the stack. :
|
||||||
|
|
||||||
|
... x [Q] dip
|
||||||
|
-------------------
|
||||||
|
... Q x
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
## Definition
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Derivation
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
## Source
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
## Discussion
|
||||||
|
|
||||||
|
## Crosslinks
|
||||||
|
|
@ -0,0 +1,42 @@
|
||||||
|
--------------
|
||||||
|
|
||||||
|
dip
|
||||||
|
^^^^^
|
||||||
|
|
||||||
|
Basis Function Combinator
|
||||||
|
|
||||||
|
|
||||||
|
The dip combinator expects a quoted program on the stack and below it
|
||||||
|
some item, it hoists the item into the expression and runs the program
|
||||||
|
on the rest of the stack.
|
||||||
|
::
|
||||||
|
|
||||||
|
... x [Q] dip
|
||||||
|
-------------------
|
||||||
|
... Q x
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
Gentzen diagram.
|
||||||
|
|
||||||
|
Definition
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Derivation
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if not basis.
|
||||||
|
|
||||||
|
Source
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
if basis
|
||||||
|
|
||||||
|
Discussion
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
|
Crosslinks
|
||||||
|
~~~~~~~~~~
|
||||||
|
|
||||||
Some files were not shown because too many files have changed in this diff Show More
Loading…
Reference in New Issue