From 5af99cc840e7d531921dad5f39666f7914f887d8 Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Thu, 17 Apr 2025 10:46:41 +0200 Subject: [PATCH] chore: fix typo in `simp` docstring (#7998) This PR fixes a typo in the `simp` hover. --- src/Init/Tactics.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean index 26b71f6180..1517f65795 100644 --- a/src/Init/Tactics.lean +++ b/src/Init/Tactics.lean @@ -1752,7 +1752,7 @@ attribute @[simp ←] and_assoc ``` When multiple simp theorems are applicable, the simplifier uses the one with highest priority. -The equational theorems of function are applied at very low priority (100 and below). +The equational theorems of functions are applied at very low priority (100 and below). If there are several with the same priority, it is uses the "most recent one". Example: ```lean @[simp high] theorem cond_true (a b : α) : cond true a b = a := rfl