Mercurial > cpdt > repo
comparison src/Reflection.v @ 479:40a9a36844d6
Batch of changes based on proofreader feedback
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Wed, 28 Nov 2012 19:33:21 -0500 |
| parents | b6c47e6d43dc |
| children | 5025a401ad9e |
comparison
equal
deleted
inserted
replaced
| 478:f02b698aadb1 | 479:40a9a36844d6 |
|---|---|
| 787 | Const n => n | 787 | Const n => n |
| 788 | Plus e1 e2 => termDenote e1 + termDenote e2 | 788 | Plus e1 e2 => termDenote e1 + termDenote e2 |
| 789 | Abs _ e1 => fun x => termDenote (e1 x) | 789 | Abs _ e1 => fun x => termDenote (e1 x) |
| 790 end. | 790 end. |
| 791 | 791 |
| 792 (** Here is a naive first attempt at a reification tactic. *) | 792 (** Here is a %\%naive first attempt at a reification tactic. *) |
| 793 | 793 |
| 794 Ltac refl' e := | 794 Ltac refl' e := |
| 795 match e with | 795 match e with |
| 796 | ?E1 + ?E2 => | 796 | ?E1 + ?E2 => |
| 797 let r1 := refl' E1 in | 797 let r1 := refl' E1 in |
| 803 constr:(Abs (fun x => r1 x)) | 803 constr:(Abs (fun x => r1 x)) |
| 804 | 804 |
| 805 | _ => constr:(Const e) | 805 | _ => constr:(Const e) |
| 806 end. | 806 end. |
| 807 | 807 |
| 808 (** Recall that a regular Ltac pattern variable [?X] only matches terms that _do not mention new variables introduced within the pattern_. In our naive implementation, the case for matching function abstractions matches the function body in a way that prevents it from mentioning the function argument! Our code above plays fast and loose with the function body in a way that leads to independent problems, but we could change the code so that it indeed handles function abstractions that ignore their arguments. | 808 (** Recall that a regular Ltac pattern variable [?X] only matches terms that _do not mention new variables introduced within the pattern_. In our %\%naive implementation, the case for matching function abstractions matches the function body in a way that prevents it from mentioning the function argument! Our code above plays fast and loose with the function body in a way that leads to independent problems, but we could change the code so that it indeed handles function abstractions that ignore their arguments. |
| 809 | 809 |
| 810 To handle functions in general, we will use the pattern variable form [@?X], which allows [X] to mention newly introduced variables that are declared explicitly. For instance: *) | 810 To handle functions in general, we will use the pattern variable form [@?X], which allows [X] to mention newly introduced variables that are declared explicitly. For instance: *) |
| 811 | 811 |
| 812 Reset refl'. | 812 Reset refl'. |
| 813 Ltac refl' e := | 813 Ltac refl' e := |