Mercurial > cpdt > repo
diff src/DataStruct.v @ 475:1fd4109f7b31
Batch of changes based on proofreader feedback
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Mon, 22 Oct 2012 14:23:52 -0400 |
parents | 218361342cd2 |
children | f02b698aadb1 |
line wrap: on
line diff
--- a/src/DataStruct.v Mon Oct 22 13:48:45 2012 -0400 +++ b/src/DataStruct.v Mon Oct 22 14:23:52 2012 -0400 @@ -311,7 +311,7 @@ | Arrow t1 t2 => typeDenote t1 -> typeDenote t2 end. -(** Now it is straightforward to write an expression interpreter. The type of the function, [expDenote], tells us that we translate expressions into functions from properly typed environments to final values. An environment for a free variable list [ts] is simply a [hlist typeDenote ts]. That is, for each free variable, the heterogeneous list that is the environment must have a value of the variable's associated type. We use [hget] to implement the [Var] case, and we use [HCons] to extend the environment in the [Abs] case. *) +(** Now it is straightforward to write an expression interpreter. The type of the function, [expDenote], tells us that we translate expressions into functions from properly typed environments to final values. An environment for a free variable list [ts] is simply an [hlist typeDenote ts]. That is, for each free variable, the heterogeneous list that is the environment must have a value of the variable's associated type. We use [hget] to implement the [Var] case, and we use [HCons] to extend the environment in the [Abs] case. *) (* EX: Define an interpreter for [exp]s. *)