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

author | wenzelm |

Thu, 12 Feb 1998 16:54:01 +0100 | |

changeset 4626 | 51dd12f34c78 |

parent 4625 | 9c6082518cfb |

child 4627 | ae95666c71cc |

tuned comments;

src/Pure/term.ML | file | annotate | diff | comparison | revisions |

--- a/src/Pure/term.ML Thu Feb 12 16:43:05 1998 +0100 +++ b/src/Pure/term.ML Thu Feb 12 16:54:01 1998 +0100 @@ -176,7 +176,7 @@ for resolution.*) type indexname = string*int; -(* Types are classified by classes. *) +(* Types are classified by sorts. *) type class = string; type sort = class list; @@ -193,7 +193,7 @@ (*terms. Bound variables are indicated by depth number. Free variables, (scheme) variables and constants have names. - An term is "closed" if there every bound variable of level "lev" + An term is "closed" if every bound variable of level "lev" is enclosed by at least "lev" abstractions. It is possible to create meaningless terms containing loose bound vars @@ -446,7 +446,7 @@ (*Substitute arguments for loose bound variables. Beta-reduction of arg(n-1)...arg0 into t replacing (Bound i) with (argi). - Note that for ((x,y)c)(a,b), the bound vars in c are x=1 and y=0 + Note that for ((%x y. c) a b), the bound vars in c are x=1 and y=0 and the appropriate call is subst_bounds([b,a], c) . Loose bound variables >=n are reduced by "n" to compensate for the disappearance of lambdas. @@ -490,7 +490,7 @@ fun ins_ix (x,xs) = if mem_ix (x, xs) then xs else x :: xs; (*Tests whether 2 terms are alpha-convertible and have same type. - Note that constants and Vars may have more than one type.*) + Note that constants may have more than one type.*) fun (Const(a,T)) aconv (Const(b,U)) = a=b andalso T=U | (Free(a,T)) aconv (Free(b,U)) = a=b andalso T=U | (Var(v,T)) aconv (Var(w,U)) = eq_ix(v,w) andalso T=U @@ -670,7 +670,7 @@ (**** Syntax-related declarations ****) -(*Dummy type for parsing. Will be replaced during type inference. *) +(*Dummy type for parsing and printing. Will be replaced during type inference. *) val dummyT = Type("dummy",[]); (*scan a numeral of the given radix, normally 10*)