## Mercurial > cpdt > repo

### comparison src/Reflection.v @ 479:40a9a36844d6

Find changesets by keywords (author, files, the commit message), revision
number or hash, or revset expression.

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 := |