Cameron Zwarich
a4f38cc782
refactor: remove code marked for deletion after old compiler ( #9280 )
2025-07-09 15:30:11 +00:00
Rob23oba
ee5b652136
doc: add documentation for builtin attributes ( #8173 )
...
This PR adds documentation to builtin attributes like `@[refl]` or
`@[implemented_by]`.
Closes #8432
---------
Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>
Co-authored-by: David Thrane Christiansen <david@lean-fro.org>
2025-06-11 09:04:37 +00:00
Henrik Böving
23e49eb519
perf: add prelude to all Lean modules
2024-02-18 14:55:17 -08:00
Mario Carneiro
dd5948d641
chore: snake-case attributes (part 1)
2022-10-19 09:28:08 -07:00
Leonardo de Moura
af99715a58
feat: store inline attribute at LCNF declarations
...
This commit also adds support for inheriting the inline attribute when
the compiler lambda lifts local functions from instances.
2022-10-13 02:06:35 -07:00
Leonardo de Moura
5606b4e59e
feat: add [alwaysInline] attribute
...
We are planning to ignore the `[inline]` attribute when the "inlining
quota" has been exhausted in the new code generator.
2022-10-12 16:08:37 -07:00
Mario Carneiro
391aef5cd7
feat: automatic extension names
2022-10-06 17:19:30 -07:00
Leonardo de Moura
85c468c853
fix: remove internal name hack at [specialize] and [inline] attributes
2022-09-23 20:25:16 -07:00
Leonardo de Moura
ee70805c35
feat: add LCNF missing cases
2022-08-06 20:23:29 -07:00
Leonardo de Moura
8de798c4a6
feat: reject [macroInline] declarations in recursive declarations
...
closes #1363
2022-07-24 07:26:35 -07:00
Leonardo de Moura
cf3b8d4eb4
chore: cleanup
...
Make the code style more uniform.
We still have a lot of leftovers from the old frontend.
2022-01-26 09:18:17 -08:00
Leonardo de Moura
0d9694d836
chore: user deriving BEq
2020-12-13 16:30:07 -08:00
Leonardo de Moura
3b6d65c3c3
chore: use deriving Inhabited
2020-12-13 10:09:20 -08:00
Leonardo de Moura
0869f38de4
chore: update structure, class, inductive
2020-11-27 15:09:30 -08:00
Leonardo de Moura
c305c2691f
chore: use :=
2020-11-19 07:22:31 -08:00
Leonardo de Moura
898a08a0c1
chore: avoid Has prefix in type classes
...
closes #203
2020-10-27 18:29:19 -07:00
Leonardo de Moura
13c2a8ff51
chore: remove #lang lean4 header
2020-10-25 09:54:07 -07:00
Leonardo de Moura
c7dc61adb9
chore: cleanup
2020-10-23 10:00:23 -07:00
Leonardo de Moura
1495f403a1
chore: use builtin_initialize instead of initialize at src/Lean
2020-10-19 15:17:02 -07:00
Leonardo de Moura
d2803d13d3
chore: move to new frontend
2020-10-17 07:10:05 -07:00
Leonardo de Moura
5ffbada3df
feat: add Lean.MonadEnv, Lean.MonadError, and Lean.MonadOptions
...
This is the first set of polymorphic methods. I will add more later,
and keep reducing code duplication.
cc @Kha
2020-08-22 16:00:43 -07:00
Leonardo de Moura
68a4c145f7
refactor: implement attribute hooks using CoreM
...
We were using a mix of `IO` and `Except`
2020-08-19 14:44:54 -07:00
Leonardo de Moura
c8ab63ea75
feat: mark auxiliary eliminators as [inline]
2020-08-10 09:41:55 -07:00
Leonardo de Moura
249bda16c0
chore: remove prelude commands from Lean package
2020-06-25 11:21:17 -07:00
Leonardo de Moura
4ccc3fef52
chore: move Init.Lean files to Lean package
2020-05-26 15:04:35 -07:00
