lean4-htt/tests
Kyle Miller a9db0d2e53
fix: use Name.appendCore instead of Name.append in unresolveNameGlobal (#3946)
`Name.append` has special handling of macro scopes, and it would cause
`unresolveNameGlobal` to panic. Using `Name.appendCore` to append name
parts is justified by the fact that it's being used to reassemble a
disassembled name.

Closes #2291
2024-04-24 15:07:18 +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 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 fix: use Name.appendCore instead of Name.append in unresolveNameGlobal (#3946) 2024-04-24 15:07:18 +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 fix: use -O3 for LLVM tests in common.sh 2023-11-02 23:21:47 +01:00
lean-toolchain doc: VS Code dev setup (#2961) 2023-11-30 08:35:03 +00:00