summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | paulson |

Wed, 03 Feb 1999 13:23:24 +0100 | |

changeset 6170 | 9a59cf8ae9b5 |

parent 6169 | f3f2560fbed9 |

child 6171 | cd237a10cbf8 |

standard spelling: type-checking

--- a/doc-src/AxClass/axclass.tex Mon Feb 01 10:29:11 1999 +0100 +++ b/doc-src/AxClass/axclass.tex Wed Feb 03 13:23:24 1999 +0100 @@ -509,7 +509,7 @@ (see \cite[page 79]{Wenzel94} for more details). On the other hand there are syntactic differences, of course. -Constants $\TIMES^\tau$ are rejected by the type checker, unless $\tau +Constants $\TIMES^\tau$ are rejected by the type-checker, unless $\tau :: \TT{product}$ is part of the type signature. In our example, this arity may be always added when required by means of a trivial \TT{instance}. @@ -549,7 +549,7 @@ \medskip While \Isa\ type classes and those of \Haskell\ are almost the same as -far as type checking and type inference are concerned, there are major +far as type-checking and type inference are concerned, there are major semantic differences. \Haskell\ classes require their instances to \E{provide operations} of certain \E{names}. Therefore, its \TT{instance} has a \TT{where} part that tells the system what these

--- a/doc-src/Intro/foundations.tex Mon Feb 01 10:29:11 1999 +0100 +++ b/doc-src/Intro/foundations.tex Wed Feb 03 13:23:24 1999 +0100 @@ -431,7 +431,7 @@ \subsection{Signatures and theories} \index{signatures|bold} -A {\bf signature} contains the information necessary for type checking, +A {\bf signature} contains the information necessary for type-checking, parsing and pretty printing a term. It specifies type classes and their relationships, types and their arities, constants and their types, etc. It also contains grammar rules, specified using mixfix declarations.

--- a/doc-src/Logics/CTT.tex Mon Feb 01 10:29:11 1999 +0100 +++ b/doc-src/Logics/CTT.tex Wed Feb 03 13:23:24 1999 +0100 @@ -541,7 +541,7 @@ uses $thms$ with the long introduction and elimination rules to solve goals of the form $a=b\in A$, where $a$ is rigid. It is intended for deriving the long rules for defined constants such as the arithmetic operators. The -tactic can also perform type checking. +tactic can also perform type-checking. \item[\ttindexbold{intr_tac} $thms$] uses $thms$ with the introduction rules to break down a type. It is @@ -607,7 +607,7 @@ \end{ttbox} These are loosely based on the intuitionistic proof procedures of~\thydx{FOL}. For the reasons discussed above, a rule that is safe for -propositional reasoning may be unsafe for type checking; thus, some of the +propositional reasoning may be unsafe for type-checking; thus, some of the `safe' tactics are misnamed. \begin{ttdescription} \item[\ttindexbold{mp_tac} $i$] @@ -729,7 +729,7 @@ This directory contains examples and experimental proofs in {\CTT}. \begin{ttdescription} \item[CTT/ex/typechk.ML] -contains simple examples of type checking and type deduction. +contains simple examples of type-checking and type deduction. \item[CTT/ex/elim.ML] contains some examples from Martin-L\"of~\cite{martinlof84}, proved using @@ -1071,7 +1071,7 @@ But a completely formal proof is hard to find. The rules can be applied in countless ways, yielding many higher-order unifiers. The proof can get bogged down in the details. But with a careful selection of derived rules -(recall Fig.\ts\ref{ctt-derived}) and the type checking tactics, we can +(recall Fig.\ts\ref{ctt-derived}) and the type-checking tactics, we can prove the theorem in nine steps. \begin{ttbox} val prems = Goal @@ -1092,7 +1092,7 @@ {\out : thm list} \end{ttbox} First, \ttindex{intr_tac} applies introduction rules and performs routine -type checking. This instantiates~$\Var{a}$ to a construction involving +type-checking. This instantiates~$\Var{a}$ to a construction involving a $\lambda$-abstraction and an ordered pair. The pair's components are themselves $\lambda$-abstractions and there is a subgoal for each. \begin{ttbox} @@ -1209,7 +1209,7 @@ {\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>} {\out ?b8(h,x) : C(x,fst(h ` x))} \end{ttbox} -Routine type checking goals proliferate in Constructive Type Theory, but +Routine type-checking goals proliferate in Constructive Type Theory, but \ttindex{typechk_tac} quickly solves them. Note the inclusion of \tdx{SumE_fst} along with the premises. \begin{ttbox} @@ -1237,7 +1237,7 @@ {\out 3. !!h x xa. [| x : A; xa : B(x) |] ==> C(x,xa) type} \end{ttbox} The proof object has reached its final form. We call \ttindex{typechk_tac} -to finish the type checking. +to finish the type-checking. \begin{ttbox} by (typechk_tac prems); {\out Level 9}

--- a/doc-src/Logics/HOL.tex Mon Feb 01 10:29:11 1999 +0100 +++ b/doc-src/Logics/HOL.tex Wed Feb 03 13:23:24 1999 +0100 @@ -28,7 +28,7 @@ \HOL\ has a distinct feel, compared with {\ZF} and {\CTT}. It identifies object-level types with meta-level types, taking advantage of -Isabelle's built-in type checker. It identifies object-level functions +Isabelle's built-in type-checker. It identifies object-level functions with meta-level functions, so it uses Isabelle's operations for abstraction and application. @@ -562,7 +562,7 @@ \begin{itemize} \item Sets are given by predicates over some type~$\sigma$. Types serve to -define universes for sets, but type checking is still significant. +define universes for sets, but type-checking is still significant. \item There is a universal set (for each type). Thus, sets have complements, and may be defined by absolute comprehension.

--- a/doc-src/Ref/classical.tex Mon Feb 01 10:29:11 1999 +0100 +++ b/doc-src/Ref/classical.tex Wed Feb 03 13:23:24 1999 +0100 @@ -773,7 +773,7 @@ search. It should estimate the size of the remaining subgoals. A good heuristic function is \ttindex{size_of_thm}, which measures the size of the proof state. Another size function might ignore certain subgoals (say, -those concerned with type checking). A heuristic function might simply +those concerned with type-checking). A heuristic function might simply count the subgoals. \item[\ttindexbold{hyp_subst_tacs}] is a list of tactics for substitution in

--- a/doc-src/Ref/goals.tex Mon Feb 01 10:29:11 1999 +0100 +++ b/doc-src/Ref/goals.tex Wed Feb 03 13:23:24 1999 +0100 @@ -622,7 +622,7 @@ \begin{ttdescription} \item[\ttindexbold{read} {\it string}] -reads the {\it string} as a term, without type checking. +reads the {\it string} as a term, without type-checking. \item[\ttindexbold{prin} {\it t};] prints the term~$t$ at the terminal.