lean4-htt/tests
Copilot d98b626633
doc: improve docstrings for simp!, simp_all!, dsimp! and autoUnfold (#9991)
- [x] Updated docstrings for `simp!`, `simp_all!`, `dsimp!` to use
user-friendly language
- [x] Updated docstrings for `autoUnfold` fields to use user-friendly
language
- [x] Fixed broken test by updating expected output for simp! hover
documentation
- [x] Replaced technical terms with clear language: "will unfold
applications of functions defined by pattern matching, when one of the
patterns applies"

<!-- START COPILOT CODING AGENT TIPS -->
---

💡 You can make Copilot smarter by setting up custom instructions,
customizing its development environment and configuring Model Context
Protocol (MCP) servers. Learn more [Copilot coding agent
tips](https://gh.io/copilot-coding-agent-tips) in the docs.

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: nomeata <148037+nomeata@users.noreply.github.com>
2025-09-09 13:34:16 +00:00
..
bench perf: improve iterator/range benchmarks, use shortcut instances for Int ranges (#10197) 2025-09-03 15:47:52 +00:00
compiler fix: Unicode path support for Lean Windows executables (#10133) 2025-08-27 11:28:55 +00:00
elabissues
ir
lean doc: improve docstrings for simp!, simp_all!, dsimp! and autoUnfold (#9991) 2025-09-09 13:34:16 +00:00
pkg perf: rebuild leak on private match (#10246) 2025-09-04 12:51:42 +00:00
playground feat: linear-size DecidableEq instance (#10152) 2025-09-03 06:31:49 +00:00
plugin
simpperf
.gitignore
common.sh
lakefile.toml
lean-toolchain