12,089
edits
Changes
Directory:Jon Awbrey/Papers/Propositions As Types (view source)
Revision as of 23:46, 25 March 2009
, 23:46, 25 March 2009→Commentary Note 1: markup
We can abbreviate this inference, that operates on two pieces of information to produce another piece of information, in the following conventional form:
We can abbreviate this inference, that operates on two pieces of information to produce another piece of information, in the following conventional form:
{| align="center" cellpadding="8" width="90%"
|
<math>\begin{array}{l}
x : X
\\
\underline{f : X \to Y}
\\
f(x) : Y
\end{array}</math>
|}
<pre>
<pre>
In this scheme of inference, the notations "x", "f", and "f(x)"
In this scheme of inference, the notations "x", "f", and "f(x)"
are taken to be names of formal objects. Some people will call
are taken to be names of formal objects. Some people will call