equal
deleted
inserted
replaced
618 \begingroup |
618 \begingroup |
619 \def\Q{{\cal Q}} |
619 \def\Q{{\cal Q}} |
620 A {\bf binder} is a variable-binding construct such as a quantifier. The |
620 A {\bf binder} is a variable-binding construct such as a quantifier. The |
621 constant declaration |
621 constant declaration |
622 \begin{ttbox} |
622 \begin{ttbox} |
623 \(c\) :: "\(\sigma\)" (binder "\(\Q\)" \(pb\) \(p\)) |
623 \(c\) :: "\(\sigma\)" (binder "\(\Q\)" [\(pb\)] \(p\)) |
624 \end{ttbox} |
624 \end{ttbox} |
625 introduces a constant~$c$ of type~$\sigma$, which must have the form |
625 introduces a constant~$c$ of type~$\sigma$, which must have the form |
626 $(\tau@1 \To \tau@2) \To \tau@3$. Its concrete syntax is $\Q~x.P$, where |
626 $(\tau@1 \To \tau@2) \To \tau@3$. Its concrete syntax is $\Q~x.P$, where |
627 $x$ is a bound variable of type~$\tau@1$, the body~$P$ has type $\tau@2$ |
627 $x$ is a bound variable of type~$\tau@1$, the body~$P$ has type $\tau@2$ |
628 and the whole term has type~$\tau@3$. The optional integer $pb$ |
628 and the whole term has type~$\tau@3$. The optional integer $pb$ |