Sebastian Ullrich
|
d4a5a2c632
|
fix: local syntax should create private definitions
|
2025-08-19 14:49:12 -07:00 |
|
Sebastian Ullrich
|
e28569f2a1
|
perf: minimize exported codegen data (#9356)
To be documented
|
2025-07-22 09:05:49 +00:00 |
|
Leonardo de Moura
|
8d2adf521d
|
feat: allow duplicate theorems to be imported
|
2024-03-13 12:57:41 -07:00 |
|
Leonardo de Moura
|
7bd005bbbe
|
test: add test for local macro in auto tactic
|
2023-01-04 09:01:02 -08:00 |
|
Leonardo de Moura
|
2b67da2854
|
fix: fixes #2000
We now add the macro scope to local syntax declarations.
|
2023-01-03 15:28:10 -08:00 |
|
Leonardo de Moura
|
1fb112f84b
|
test: Environment.addExtraName
|
2022-09-21 15:03:11 -07:00 |
|