lean4-htt/tests
Kyle Miller d3f7ed434b
fix: automatic instance names about types with hygienic names should be hygienic (#5530)
Macros sometimes create auxiliary types and instances about them, and
they rely on the instance name generate to create unique names in that
case.

This modifies the automatic name generator to add a fresh macro scope to
the generated name if any of the constants in the type of the instance
themselves have macro scopes.

Closes #2044
2024-09-30 16:06:36 +00:00
..
bench chore: notation ^^ for Bool.xor (#5332) 2024-09-18 08:59:11 +00:00
compiler doc: update documentation and tests for toUIntX functions (#5497) 2024-09-29 08:11:04 +00:00
elabissues
ir
lean fix: automatic instance names about types with hygienic names should be hygienic (#5530) 2024-09-30 16:06:36 +00:00
pkg test: check that recusive functions do not apply attriubutes twices (#5480) 2024-09-26 10:30:37 +00:00
playground chore: fix spelling mistakes in tests (#5439) 2024-09-24 03:22:53 +00:00
plugin
simpperf
.gitignore
common.sh
lean-toolchain