max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: fix typo in simp docstring (#7998)

Browse source 
This PR fixes a typo in the `simp` hover.
This commit is contained in:
Markus Himmel 2025-04-17 10:46:41 +02:00 • committed by GitHub
parent 85f5a81f17
commit 5af99cc840
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Tactics.lean
View file

@ -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