lean4-htt/tests
Kyle Miller d569ed4e5f
feat: make loose fvars pretty print as _fvar.123 instead of _uniq.123 (#3380)
Loose fvars are never supposed to be pretty printed, but having them
print with "fvar" in the name can help with debugging broken tactics and
elaborators.

Metaprogramming users often do not realize at first that `_uniq.???` in
pretty printing output refers to fvars not in the current local context.
2024-02-18 01:53:37 +00:00
..
bench fix: liasolver benchmark bug introduced by #3364 (#3372) 2024-02-16 23:39:26 +00:00
compiler
elabissues feat: add bitwise operations to reduceNat? and kernel (#3134) 2024-01-11 18:12:45 +00:00
ir feat: lake: GNU/BSD OS detection in test scripts (#3180) 2024-01-14 02:49:38 +00:00
lean feat: make loose fvars pretty print as _fvar.123 instead of _uniq.123 (#3380) 2024-02-18 01:53:37 +00:00
pkg feat: simproc sets 2024-02-01 16:58:54 +11:00
playground
plugin
simpperf
.gitignore
common.sh
lean-toolchain doc: VS Code dev setup (#2961) 2023-11-30 08:35:03 +00:00