Mercurial > cpdt > repo
comparison src/StackMachine.v @ 492:fa2eb72446a8
Pass through Chapter 2
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Fri, 18 Jan 2013 14:22:50 -0500 |
parents | 1fd4109f7b31 |
children | a4b3386ae140 |
comparison
equal
deleted
inserted
replaced
491:da576746c3ba | 492:fa2eb72446a8 |
---|---|
398 : forall (A : Type) (l m n : list A), (l ++ m) ++ n = l ++ m ++ n | 398 : forall (A : Type) (l m n : list A), (l ++ m) ++ n = l ++ m ++ n |
399 | 399 |
400 ]] | 400 ]] |
401 | 401 |
402 If we did not already know the name of the theorem, we could use the %\index{Vernacular commands!SearchRewrite}%[SearchRewrite] command to find it, based on a pattern that we would like to rewrite: *) | 402 If we did not already know the name of the theorem, we could use the %\index{Vernacular commands!SearchRewrite}%[SearchRewrite] command to find it, based on a pattern that we would like to rewrite: *) |
403 | |
404 (* begin hide *) | |
405 (* begin thide *) | |
406 Definition bleh := app_assoc. | |
407 (* end thide *) | |
408 (* end hide *) | |
403 | 409 |
404 SearchRewrite ((_ ++ _) ++ _). | 410 SearchRewrite ((_ ++ _) ++ _). |
405 (** %\vspace{-.15in}%[[ | 411 (** %\vspace{-.15in}%[[ |
406 app_assoc_reverse: | 412 app_assoc_reverse: |
407 forall (A : Type) (l m n : list A), (l ++ m) ++ n = l ++ m ++ n | 413 forall (A : Type) (l m n : list A), (l ++ m) ++ n = l ++ m ++ n |