Mercurial > cpdt > repo

comparison src/DeBruijn.v @ 291:da9ccc6bf572

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
PC comments for DeBruijn
author Adam Chlipala <adam@chlipala.net>
date Wed, 10 Nov 2010 15:42:05 -0500
parents dce88a5c170c
children 7b38729be069
comparison
equal deleted inserted replaced
290:758778c0468c 291:da9ccc6bf572
1 (* Copyright (c) 2009, Adam Chlipala 1 (* Copyright (c) 2009-2010, Adam Chlipala
2 * 2 *
3 * This work is licensed under a 3 * This work is licensed under a
4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
5 * Unported License. 5 * Unported License.
6 * The license text is available at: 6 * The license text is available at:
148 | _ => idtac 148 | _ => idtac
149 end] 149 end]
150 end). 150 end).
151 (* end hide *) 151 (* end hide *)
152 152
153 (** Less than a page of tactic code will be sufficient to automate our proof of commuativity. We start by defining a workhorse simplification tactic [simp], which extends [crush] in a few ways. 153 (** Less than a page of tactic code will be sufficient to automate our proof of commutativity. We start by defining a workhorse simplification tactic [simp], which extends [crush] in a few ways.
154 154
155 [[ 155 [[
156 Ltac simp := repeat progress (crush; try discriminate; 156 Ltac simp := repeat progress (crush; try discriminate;
157 157
158 ]] 158 ]]