From ce8a5c3804c50a4ee33f54b6f2fd8c6421b8cca1 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Sat, 25 Jun 2016 18:55:33 -0400 Subject: s/on// --- folkwisdom.md | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'folkwisdom.md') 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 -- cgit v1.2.3