lean4-htt/tests
Rob23oba e450a02621
fix: change show tactic to work as documented (#7395)
This PR changes the `show t` tactic to match its documentation.
Previously it was a synonym for `change t`, but now it finds the first
goal that unifies with the term `t` and moves it to the front of the
goal list.
2025-06-12 23:54:09 +00:00
..
bench chore: lean --stats gives number of imported bytes (#8725) 2025-06-12 08:29:42 +00:00
compiler fix: remove incorrect strictOr/strictAnd optimizations (#8594) 2025-06-02 16:14:56 +00:00
elabissues
ir
lean fix: change show tactic to work as documented (#7395) 2025-06-12 23:54:09 +00:00
pkg feat: explicit defeq attribute (#8419) 2025-06-06 18:40:06 +00:00
playground
plugin
simpperf
.gitignore
common.sh
lean-toolchain