diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-06-25 18:58:01 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-06-25 18:58:01 -0400 |
| commit | 1554ea63676e285b8e8959bba6331a5ad11810d6 (patch) | |
| tree | 08b786a0e796428284d8ebe52921aae471d6bff6 /folkwisdom.md | |
| parent | ce8a5c3804c50a4ee33f54b6f2fd8c6421b8cca1 (diff) | |
recommend pose proof instead of pose
Diffstat (limited to 'folkwisdom.md')
| -rw-r--r-- | folkwisdom.md | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/folkwisdom.md b/folkwisdom.md index 079056439..4f6d354eb 100644 --- a/folkwisdom.md +++ b/folkwisdom.md @@ -207,12 +207,12 @@ not reveal the issue, try `setoid_rewrite` instead for troubleshooting (it sometimes even gives sensible error messages in Coq 8.5) but revert to `rewrite` once the issue has been found and fixed. If rewriting picks the wrong `Equivalence` or `Proper` instance for some type or function (or fails to find -one altogether), troubleshoot that separately: check that `pose (_:@Equivalence -T equiv)` or `pose(_:Proper (equiv1==>equiv2) f)` give the right answer, and if -not, `Set Typeclasses Debug` and read the log (which is in the hidden `*coq*` -buffer in `proofgeneral`). A useful heuristic for reading that log is to look -for the first place where the resolution backtracks and then read backwards from -there. +one altogether), troubleshoot that separately: check that `pose proof +(_:@Equivalence T equiv)` or `pose(_:Proper (equiv1==>equiv2) f)` give the right +answer, and if not, `Set Typeclasses Debug` and read the log (which is in the +hidden `*coq*` buffer in `proofgeneral`). A useful heuristic for reading that +log is to look for the first place where the resolution backtracks and then read +backwards from there. 5. To perform multiple rewrites at once, make rewrite hint database and call `(rewrite_strat topdown hints dbname).` where `topdown` can be replaced with `bottomup` for different behavior. This does not seem to unfold |