Mercurial > cpdt > repo

comparison src/Large.v @ 452:980962258b49

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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