summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

doc-src/Logics/CTT.tex

changeset 6170 | 9a59cf8ae9b5 |

parent 6072 | 5583261db33d |

child 7159 | b009afd1ace5 |

--- 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}