Leonardo de Moura
173b956961
feat: reserved names ( #3675 )
...
- Add support for reserved declaration names. We use them for theorems
generated on demand.
- Equation theorems are not private declarations anymore.
- Generate equation theorems on demand when resolving symbols.
- Prevent users from creating declarations using reserved names. Users
can bypass it using meta-programming.
See next test for examples.
2024-03-15 00:33:22 +00:00
Joe Hendrix
29244f32f6
chore: upstream solve_by_elim ( #3408 )
...
This upstreams the solve_by_elim tactic from Std.
It is a key tactic needed by library_search.
2024-02-21 01:16:04 +00:00
Mario Carneiro
c4cbefce11
feat: add linter.deprecated option to silence deprecation warnings
2022-10-23 21:11:57 +02:00
Leonardo de Moura
b6e9d58537
feat: add [deprecated] attribute
2022-07-24 18:06:03 -07:00
E.W.Ayers
1785ab142e
refactor: move Lean.PrettyPrinter.Delaborator.SubExpr to Lean.SubExpr
...
This is because SubExpr has uses outside the Delaborator.
Closes #1183
2022-06-03 12:38:14 -07:00
larsk21
37d5f8e74a
feat: add unused variables linter
2022-06-03 13:03:52 +02:00
Leonardo de Moura
caa79ca04f
refactor: move MonadLog
2022-05-31 16:50:48 -07:00
tydeu
a3250dc44b
feat: expose --load-dynlib functionality to Lean code
2021-12-15 08:26:48 +00:00
Wojciech Nawrocki
6eaa536595
feat: pretty-printer with tags
2021-08-24 08:57:41 -07:00
Leonardo de Moura
34b092700e
feat: add LazyInitExtension
2021-08-16 12:54:50 -07:00
Leonardo de Moura
be33ca69cd
feat: environment extension for storing declaration ranges
2021-01-10 18:25:56 -08:00
Leonardo de Moura
2c8001a7f3
feat: add DocString.lean
2021-01-10 07:13:33 -08:00
Leonardo de Moura
5f5a8010a2
feat: add ScopedEnvExtension
2020-12-03 17:04:16 -08:00
Sebastian Ullrich
f6816a0ffa
refactor: move & split Lean.Delaborator
2020-11-30 13:52:46 +01:00
Sebastian Ullrich
feedb539cd
chore: import orphaned files in Lean
2020-11-24 19:16:27 +01:00
Sebastian Ullrich
c1d75e21ea
fix: fix pretty printers for imported ParserDescrs
...
... by interpreting them (imported or not) on the fly instead of storing them in the environment
/cc @leodemoura
2020-11-07 17:05:07 +01:00
Leonardo de Moura
3de97ddc27
feat: run linters in the new frontend
2020-10-23 14:04:28 -07:00
Leonardo de Moura
eacf3ed6c7
refactor: move ResolveName to Lean directory
2020-10-10 11:07:14 -07:00
Leonardo de Moura
4faaa392b3
feat: add InternalExceptionId.lean
2020-08-21 13:06:31 -07:00
Sebastian Ullrich
68b9a8e1d1
refactor: move parenthesizer compiler into separate file, generalize
2020-08-20 13:22:57 +02:00
Leonardo de Moura
b142c608fe
feat: add CoreM
2020-08-18 09:45:16 -07:00
Leonardo de Moura
e818368c96
refactor: move EqnCompiler to Meta folder
2020-08-06 09:10:01 -07:00
Leonardo de Moura
4ccc3fef52
chore: move Init.Lean files to Lean package
2020-05-26 15:04:35 -07:00
Leonardo de Moura
f7818757ef
chore: add Lean package to CMakeLists.txt
2020-05-26 13:50:04 -07:00
Leonardo de Moura
8d30f67823
feat: add Lean package
2020-05-26 13:39:03 -07:00
