max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/Lean/Compiler
History
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
..
IR perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
LCNF fix: regression on match expressions with builtin literals (#3521) 2024-02-27 18:49:44 +00:00
AtMostOnce.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
BorrowedAnnotation.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
ClosedTermCache.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
ConstFolding.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
CSimpAttr.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
ExportAttr.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
ExternAttr.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
FFI.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
ImplementedByAttr.lean feat: reserved names (#3675) 2024-03-15 00:33:22 +00:00
InitAttr.lean feat: reserved names (#3675) 2024-03-15 00:33:22 +00:00
InlineAttrs.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
IR.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
LCNF.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Main.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
NameMangling.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
NeverExtractAttr.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
NoncomputableAttr.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Old.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Options.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00
Specialize.lean perf: add prelude to all Lean modules 2024-02-18 14:55:17 -08:00