diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-06-25 18:55:33 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-06-25 18:55:33 -0400 |
| commit | ce8a5c3804c50a4ee33f54b6f2fd8c6421b8cca1 (patch) | |
| tree | 11075c3d4e0d1189ebc8dee6b45f9059e08f7db3 /folkwisdom.md | |
| parent | fb7b8555839b38a36ca877650b2198685f9ffa34 (diff) | |
s/on//
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 687b09993..079056439 100644 --- a/folkwisdom.md +++ b/folkwisdom.md @@ -166,12 +166,12 @@ be instantiated with a type whose propositional equivalence makes little sense, it is well worth requiring additional parameters for `Proper` and `Equivalence` (and maybe `Decidable`) instances. See the Algebra library for an example. -When writing a tactic, specify on the form of the input goal format with -syntactic precision -- trying to be insensitive to syntactic changes and only -require definitional equality can lead to arbitrary amounts of computation and -is usually not worth it. One possible exception is the -reification-by-typeclasses pattern which has not yet had issues even when it -works up to definitional equivalence to the extent typeclass resolution does. +When writing a tactic, specify the form of the input goal format with syntactic +precision -- trying to be insensitive to syntactic changes and only require +definitional equality can lead to arbitrary amounts of computation and is +usually not worth it. One possible exception is the reification-by-typeclasses +pattern which has not yet had issues even when it works up to definitional +equivalence to the extent typeclass resolution does. ### Custom Equivalence Relations and Tactics |