Mercurial > cpdt > repo
comparison src/Large.v @ 452:980962258b49
Typo fixes
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Thu, 23 Aug 2012 11:06:37 -0400 |
parents | 0650420c127b |
children | d7a73ab1df7b |
comparison
equal
deleted
inserted
replaced
451:822442bf6d7f | 452:980962258b49 |
---|---|
47 match e with | 47 match e with |
48 | Const n => Const (k * n) | 48 | Const n => Const (k * n) |
49 | Plus e1 e2 => Plus (times k e1) (times k e2) | 49 | Plus e1 e2 => Plus (times k e1) (times k e2) |
50 end. | 50 end. |
51 | 51 |
52 (** We can write a very manual proof that [double] really doubles an expression's value. *) | 52 (** We can write a very manual proof that [times] really implements multiplication. *) |
53 | 53 |
54 Theorem eval_times : forall k e, | 54 Theorem eval_times : forall k e, |
55 eval (times k e) = k * eval e. | 55 eval (times k e) = k * eval e. |
56 induction e. | 56 induction e. |
57 | 57 |