This PR uses the linter from https://github.com/leanprover/lean4/pull/8901 to clean up simp arguments. |
||
|---|---|---|
| .. | ||
| Basic.lean | ||
| Extra.lean | ||
| Lemmas.lean | ||
This PR uses the linter from https://github.com/leanprover/lean4/pull/8901 to clean up simp arguments. |
||
|---|---|---|
| .. | ||
| Basic.lean | ||
| Extra.lean | ||
| Lemmas.lean | ||