undefined | Better HN

0 pointsUltraSane9mo ago0 comments

This is NOT what Lean 4 is designed to do. You seem to be using Lean 4 for what TLA+ is much better suited for.

0 comments

If it is not suitable for programming, then it should not be branded as a programming language. Heck, its homepage says:

> Lean's metaprogramming capabilities enable users to extend the language with domain-specific notations and new proof automation techniques.

j / k navigate · click thread line to collapse

If it is not suitable for programming, then it should not be branded as a programming language. Heck, its homepage says:

> Lean's metaprogramming capabilities enable users to extend the language with domain-specific notations and new proof automation techniques.

j / k navigate · click thread line to collapse