diff options
| author |  Andres Erbsen <andres@krutt.org> | 2016-06-24 17:15:59 -0400 |
|---|---|---|
| committer |  GitHub <noreply@github.com> | 2016-06-24 17:15:59 -0400 |
| commit | 3c36b589a01bce19063872544bca132f3daf947d (patch) | |
| tree | 79718762c10ec63bf7293c7419514e5fe021bae1 | |
| parent | 54e43d2c5f8c2f095bda4ff19ad56153369f2630 (diff) | |
folkwisdom: remove redundant idtac
| -rw-r--r-- | folkwisdom.md | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/folkwisdom.md b/folkwisdom.md index d87174115..c6190a460 100644 --- a/folkwisdom.md +++ b/folkwisdom.md @@ -211,7 +211,7 @@ 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 -`idtac; (rewrite_strat topdown hints dbname).` where `topdown` can be replaced +`(rewrite_strat topdown hints dbname).` where `topdown` can be replaced with `bottomup` for different behavior. This does not seem to unfold definitions, so it may be a reasonable alternative to using `Local Opaque` to protect definitions from `setoid_rewrite`. |