The Lean module system
Sebastian Ullrich (Lean FRO)
Tue Jan 20, 14:30-15:00 (4 weeks ago)
Abstract: The module system is a new extension of the Lean language that allows for more control over the public interface of Lean files, considerably increasing robustness and scalability of libraries in multiple aspects. In this talk, I will cover the basics of the module system and what impact we are already seeing from its adoption in Mathlib and beyond.
More info: * lean-lang.org/doc/reference/latest/Source-Files-and-Modules/#module-scopes * drive.google.com/file/d/1AyaYBwnYON_bq3aWjS-Nr3b4vne7c4SJ/view ("Optimizing Lean Libraries using the Module System" starts at 1:06:25)
logic in computer sciencemathematical softwareMathematics
Audience: researchers in the discipline
| Organizer: | Jireh Loreaux* |
| *contact for this listing |
Export talk to