Commit 2023-11-20 10:21 c21c11f1
View on Github →chore: exact? runs nonspecific lemmas too (#8459)
Previously, exact?
has only indexed lemmas with a "specific" DiscrTree
key (this meant: anything except #[star]
or #[Eq, star, star, star]
).
This means that it wouldn't apply some very general lemmas, e.g. le_antisymm
.
The performance improvement here is pretty minor: the DiscrTree
returns the more specific matches first, so we only attempt to apply the nonspecific keys last (i.e. if we would otherwise have already failed).