16.2. 最小化 grind 调用🔗

grind only [...]策略使用一组有限的定理调用 grind，这可以提高性能。 可以使用 grind? 方便地构造对 grind only 的调用，它会自动记录 grind 使用的定理并建议合适的 grind only。

这些定理通常包含符号前缀，例如 =、← 或 →，表示 触发实例化的模式。详细信息请参见 电子匹配部分。 某些定理可能标有 usr 前缀，这表示使用了自定义模式。