I've been reading up on Church's simple type theory and much of the concepts make sense to me. However, I can't actually figure out how to define functions explicitly using the notation provided.
Notationally, let's say that $\ast$ is the type of boolean truth values, and that $T$ and $F$ are the two constants of that type.
Suppose that I want to define some basic logic gates in STT. The NOT gate is going to be of type $(\ast \to \ast)$, and we can define as $\lambda x:\ast. (x=F)$.
For XNOR, we can curry to obtain a gate of type $(\ast \to (\ast \to \ast))$, which we can define as $\lambda x:\ast. \lambda y:\ast. (x=y)$.
For XOR, we can instead go with $\lambda x:\ast. \lambda y:\ast. ((x=y)=F)$.
But how do we handle something like AND, OR, etc?
In general, is there any way to specify a boolean function by specifying its truth table, or something like that?
EDIT: to be clear, I'm not looking at their embedding of propositional logic into STT further down the page, where they have alternate definitions of $\mathsf{T}$ and $\mathsf{F}$ that differ from the primitive constants $\small{T}$ and $\small{F}$. I'm just trying to figure out how to define functions, period, and I'm using the type $\ast$ for the sake of constructing simple examples.
In short, I want to figure out how to explicitly define a function of type $(\ast \to (\ast \to \ast))$, or $(\ast \to (\ast \to (\ast \to \ast)))$, and so on. How do I do that?
The paper gives a definition of AND and OR when it describes the embedding of propositional logic into STT. In particular, AND was defined as: $$A_*\land B_* \equiv (\lambda f:* \to * \to *.f(\mathsf{T})(\mathsf{T}))=(\lambda f:*\to*\to *.f(A_*)(B_*))$$
Given $\neg$ and $\land$, we can define the other classical propositional connectives as usual which is what they proceed to do.
You can understand this definition as $$A_*\land B_*\equiv \langle\mathsf{T},\mathsf{T}\rangle = \langle A_*, B_* \rangle$$ where $\langle A_*, B_* \rangle$ represents the pair of $A_*$ and $B_*$. Of course, the calculus presented doesn't have pairs, so a Church-encoded representation is used instead. You could then, if you like, directly encode OR as the Church-encoded form of $A_*\lor B_* \equiv\langle\mathsf{F},\mathsf{F}\rangle\neq\langle A_*,B_*\rangle$.
Alternatively, you can use the $\mathsf{if}$ construct defined via definite description to simply define whichever Boolean function you want via cases, though I'd personally prefer not relying on definite description.
You can also peruse the definitions used in implementations, such as this one from HOL Light: https://github.com/jrh13/hol-light/blob/7ea931a7d9925fa4abaa14767ba2510c0ad28c62/bool.ml#L97 You can see that it is the definition above.