Mercurial > cpdt > repo
comparison src/MoreDep.v @ 465:4320c1a967c2
Spell check
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Wed, 29 Aug 2012 18:26:26 -0400 |
| parents | 49bd155dfc52 |
| children | 1fd4109f7b31 |
comparison
equal
deleted
inserted
replaced
| 464:e53d051681b0 | 465:4320c1a967c2 |
|---|---|
| 208 | Nat => nat | 208 | Nat => nat |
| 209 | Bool => bool | 209 | Bool => bool |
| 210 | Prod t1 t2 => typeDenote t1 * typeDenote t2 | 210 | Prod t1 t2 => typeDenote t1 * typeDenote t2 |
| 211 end%type. | 211 end%type. |
| 212 | 212 |
| 213 (** The [typeDenote] function compiles types of our object language into "native" Coq types. It is deceptively easy to implement. The only new thing we see is the [%]%\coqdocvar{%#<tt>#type#</tt>#%}% annotation, which tells Coq to parse the [match] expression using the notations associated with types. Without this annotation, the [*] would be interpreted as multiplication on naturals, rather than as the product type constructor. The token %\coqdocvar{%#<tt>#type#</tt>#%}% is one example of an identifer bound to a%\index{notation scope delimiter}% _notation scope delimiter_. In this book, we will not go into more detail on notation scopes, but the Coq manual can be consulted for more information. | 213 (** The [typeDenote] function compiles types of our object language into "native" Coq types. It is deceptively easy to implement. The only new thing we see is the [%]%\coqdocvar{%#<tt>#type#</tt>#%}% annotation, which tells Coq to parse the [match] expression using the notations associated with types. Without this annotation, the [*] would be interpreted as multiplication on naturals, rather than as the product type constructor. The token %\coqdocvar{%#<tt>#type#</tt>#%}% is one example of an identifier bound to a%\index{notation scope delimiter}% _notation scope delimiter_. In this book, we will not go into more detail on notation scopes, but the Coq manual can be consulted for more information. |
| 214 | 214 |
| 215 We can define a function [expDenote] that is typed in terms of [typeDenote]. *) | 215 We can define a function [expDenote] that is typed in terms of [typeDenote]. *) |
| 216 | 216 |
| 217 Fixpoint expDenote t (e : exp t) : typeDenote t := | 217 Fixpoint expDenote t (e : exp t) : typeDenote t := |
| 218 match e with | 218 match e with |