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 |