Commit 2023-11-20 10:21 c21c11f1

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).