16.2. 最小化 grind 调用🔗

grind only [...] 策略使用受限的定理集合调用 grind，从而可能提升性能。 可以使用 grind? 方便地构造 grind only 调用；它会自动记录 grind 使用的定理，并建议合适的 grind only。

这些定理通常带有 =、← 或 → 等符号前缀，用来表示 触发实例化的模式。详情参见关于 E-匹配的章节。 有些定理可能带有 usr 前缀，表示使用了自定义模式。