Mercurial > cpdt > repo
comparison src/Subset.v @ 341:e76aced46eb1
Typo fix
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Sun, 16 Oct 2011 08:54:36 -0400 |
parents | aaeba4cfd075 |
children | 549d604c3d16 |
comparison
equal
deleted
inserted
replaced
340:23b06f87bd30 | 341:e76aced46eb1 |
---|---|
405 *) | 405 *) |
406 | 406 |
407 Eval compute in eq_nat_dec 2 3. | 407 Eval compute in eq_nat_dec 2 3. |
408 (** %\vspace{-.15in}% [[ | 408 (** %\vspace{-.15in}% [[ |
409 = No | 409 = No |
410 : {2 = 2} + {2 <> 2} | 410 : {2 = 3} + {2 <> 3} |
411 ]] | 411 ]] |
412 *) | 412 *) |
413 | 413 |
414 (** Note that the [Yes] and [No] notations are hiding proofs establishing the correctness of the outputs. | 414 (** Note that the [Yes] and [No] notations are hiding proofs establishing the correctness of the outputs. |
415 | 415 |