3 ms·
that is a neat demo with a lot of useful links! In fact, it seems that the Lean developers/community are very interested in new methods of achieving readability
by asdftemp 6y ago
that is a neat demo with a lot of useful links! In fact, it seems that the Lean developers/community are very interested in new methods of achieving readability, and providing users with tools to build interfaces that scale up to the complexity of real workflows.
For example, Lean in vscode supports interactive html "widgets": https://youtu.be/8NUBQEZYuis?t=453 https://youtu.be/8NUBQEZYuis?t=453
(at that timestamp, there's a quick introduction to their typical use at the moment).
lean4 is committed to all sorts of extensibility; here's a demonstration of the new macros: https://twitter.com/derKha/status/1354082976456441861 https://twitter.com/derKha/status/1354082976456441861. There have also been several instances of users implementing old lean3 features (for example, the `calc` tactic mode, which has unique syntax for proving (in)equalities) by simply defining new type classes and short macros.