lean4-htt/tests
Kim Morrison d2eb1bc9f5
chore: review of failing grind tests (#10166)
This PR reviews the expected-to-fail-right-now tests for `grind`, moving
some (now passing) tests to the main test suite, updating some tests,
and adding some tests about normalisation of exponents.
2025-08-28 05:24:31 +00:00
..
bench perf: do not export opaque bodies (#10119) 2025-08-27 20:59:59 +00:00
compiler fix: Unicode path support for Lean Windows executables (#10133) 2025-08-27 11:28:55 +00:00
elabissues
ir
lean chore: review of failing grind tests (#10166) 2025-08-28 05:24:31 +00:00
pkg chore: improve error message on trying to access an identifier imported privately from the public scope (#10153) 2025-08-27 13:43:56 +00:00
playground chore: eliminate uses of intros x y z (#9983) 2025-08-19 06:09:13 +00:00
plugin
simpperf
.gitignore
common.sh
lakefile.toml
lean-toolchain