lean4-htt/tests
François G. Dorais 05b68687c0
feat: #print command shows structure fields (#3768)
<!--
# Read this section before submitting

* Ensure your PR follows the [External Contribution
Guidelines](https://github.com/leanprover/lean4/blob/master/CONTRIBUTING.md).
* Please make sure the PR has excellent documentation and tests. If we
label it `missing documentation` or `missing tests` then it needs
fixing!
* Include the link to your `RFC` or `bug` issue in the description.
* If the issue does not already have approval from a developer, submit
the PR as draft.
* The PR title/description will become the commit message. Keep it
up-to-date as the PR evolves.
* If you rebase your PR onto `nightly-with-mathlib` then CI will test
Mathlib against your PR.
* You can manage the `awaiting-review`, `awaiting-author`, and `WIP`
labels yourself, by writing a comment containing one of these labels on
its own line.
* Remove this section, up to and including the `---` before submitting.
-->
See RFC #3644 for a discussion of design choices.

Closes #3644
2024-04-24 03:18:09 +00:00
..
bench chore: Nat.repr microbenchmark (#3888) 2024-04-17 18:10:32 +00:00
compiler fix: do not dllexport symbols in core static libraries (#3601) 2024-03-15 11:58:34 +00:00
elabissues
ir
lean feat: #print command shows structure fields (#3768) 2024-04-24 03:18:09 +00:00
pkg feat: lake: alternative TOML config (#3298) 2024-03-28 02:35:02 +00:00
playground chore: bool and prop lemmas for Mathlib compatibility and improved confluence (#3508) 2024-03-04 23:56:30 +00:00
plugin fix: do not dllexport symbols in core static libraries (#3601) 2024-03-15 11:58:34 +00:00
simpperf
.gitignore
common.sh
lean-toolchain