Mercurial > cpdt > repo
comparison src/StackMachine.v @ 465:4320c1a967c2
Spell check
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Wed, 29 Aug 2012 18:26:26 -0400 |
| parents | 980962258b49 |
| children | b4dd18787d04 |
comparison
equal
deleted
inserted
replaced
| 464:e53d051681b0 | 465:4320c1a967c2 |
|---|---|
| 692 << | 692 << |
| 693 The term "(n, s)" has type "(nat * vstack ts)%type" | 693 The term "(n, s)" has type "(nat * vstack ts)%type" |
| 694 while it is expected to have type "vstack ?119". | 694 while it is expected to have type "vstack ?119". |
| 695 >> | 695 >> |
| 696 | 696 |
| 697 This and other mysteries of Coq dependent typing we postpone until Part II of the book. The upshot of our later discussion is that it is often useful to push inside of [match] branches those function parameters whose types depend on the type of the value being matched. Our later, more complete treatement of Gallina's typing rules will explain why this helps. | 697 This and other mysteries of Coq dependent typing we postpone until Part II of the book. The upshot of our later discussion is that it is often useful to push inside of [match] branches those function parameters whose types depend on the type of the value being matched. Our later, more complete treatment of Gallina's typing rules will explain why this helps. |
| 698 *) | 698 *) |
| 699 | 699 |
| 700 (** We finish the semantics with a straightforward definition of program denotation. *) | 700 (** We finish the semantics with a straightforward definition of program denotation. *) |
| 701 | 701 |
| 702 Fixpoint tprogDenote ts ts' (p : tprog ts ts') : vstack ts -> vstack ts' := | 702 Fixpoint tprogDenote ts ts' (p : tprog ts ts') : vstack ts -> vstack ts' := |