Lines Matching refs:function
115 \index{*"` symbol}\index{function applications!in CTT}
119 \tt ` & $[i,i]\to i$ & Left 55 & function application\\
135 \rm function space $A\to B$ \\
170 the function application operator (sometimes called `apply'), and the 2-place
173 \hbox{\tt lam $x$. $b$} and $b{\tt`}a$. A CTT function~$f$ is simply an
424 it can even express Ackermann's function, which is not primitive recursive
428 include function types as a special case. The rules correspond to the
722 the predecessor function is $\lambda v. {\tt rec}(v, 0, \lambda x\,y. x)$.
757 predecessor function on the natural numbers.
799 $\prod@{x\in N}N$, which is shown as the function type $N\to N$ because
991 The functional takes a function~$f$ that maps $z:\Sigma(A,B)$
992 to~$C(z)$; the resulting function maps $x\in A$ and $y\in B(x)$ to
1037 Using $\Pi$-elimination, we solve subgoal~1 by applying the function~$f$.
1046 Finally, we verify that the argument's type is suitable for the function
1062 Suppose we have a function $h\in \prod@{x\in A}\sum@{y\in B(x)} C(x,y)$,
1066 that we can construct a function $f\in \prod@{x\in A}B(x)$ such that
1068 function $g\in \prod@{x\in A}C(x,f{\tt`}x)$.
1118 Subgoal~1 asks to find the choice function itself, taking $x\in A$ to some
1120 object $\Var{b@8}(h,x)$ to witness that the choice function's argument and
1136 Above, we have composed {\tt fst} with the function~$h$. Unification
1137 has deduced that the function must be applied to $x\in A$. We have our
1138 choice function.