Mercurial > cpdt > repo
comparison src/Reflection.v @ 485:2d66421b8aa1
Small wording change suggested by a proofreader
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Sun, 06 Jan 2013 16:34:22 -0500 |
| parents | 5025a401ad9e |
| children | 36428dfcde84 |
comparison
equal
deleted
inserted
replaced
| 484:5025a401ad9e | 485:2d66421b8aa1 |
|---|---|
| 657 (** ** Manual Reification of Terms with Variables *) | 657 (** ** Manual Reification of Terms with Variables *) |
| 658 | 658 |
| 659 (* begin thide *) | 659 (* begin thide *) |
| 660 (** The action of the [quote] tactic above may seem like magic. Somehow it performs equality comparison between subterms of arbitrary types, so that these subterms may be represented with the same reified variable. While [quote] is implemented in OCaml, we can code the reification process completely in Ltac, as well. To make our job simpler, we will represent variables as [nat]s, indexing into a simple list of variable values that may be referenced. | 660 (** The action of the [quote] tactic above may seem like magic. Somehow it performs equality comparison between subterms of arbitrary types, so that these subterms may be represented with the same reified variable. While [quote] is implemented in OCaml, we can code the reification process completely in Ltac, as well. To make our job simpler, we will represent variables as [nat]s, indexing into a simple list of variable values that may be referenced. |
| 661 | 661 |
| 662 Step one of the process is to crawl over a term, building a duplicate-free list of all values that appear in positions we will encode as variables. A useful helper function adds an element to a list, maintaining lack of duplicates. Note how we use Ltac pattern matching to implement an equality test on Gallina terms; this is simple syntactic equality, not even the richer definitional equality. We also represent lists as nested tuples, to allow different list elements to have different Gallina types. *) | 662 Step one of the process is to crawl over a term, building a duplicate-free list of all values that appear in positions we will encode as variables. A useful helper function adds an element to a list, preventing duplicates. Note how we use Ltac pattern matching to implement an equality test on Gallina terms; this is simple syntactic equality, not even the richer definitional equality. We also represent lists as nested tuples, to allow different list elements to have different Gallina types. *) |
| 663 | 663 |
| 664 Ltac inList x xs := | 664 Ltac inList x xs := |
| 665 match xs with | 665 match xs with |
| 666 | tt => false | 666 | tt => false |
| 667 | (x, _) => true | 667 | (x, _) => true |