Lines Matching defs:over
140 where the type variable~$\alpha$ ranges over all types.
234 over type~$nat$. This is true if $P(x)$ is true for all~$x$. Abstracting
251 Quantifiers may be polymorphic. We may define $\forall$ and~$\exists$ over
253 allow summations over all arithmetic types:
280 Equalities left over from the unification process, so called {\bf
299 $\alpha{::}\{\}$ ranges over the universal sort.
698 \subsection{Lifting over assumptions}
699 \index{assumptions!lifting over}
700 Lifting over $\theta\Imp{}$ is the following meta-inference rule:
706 $\phi$ must be true. Iterated lifting over a series of meta-formulae
716 renames the unknowns to $\Var{P@1}$ and $\Var{Q@1}$, then lifts the rule over
731 \subsection{Lifting over parameters}
732 \index{parameters!lifting over}
743 where $\phi^x$ stands for the result of lifting unknowns over~$x$ in
808 lifting over subgoal~$i$'s assumptions and parameters. If the proof state