Some quick info for Lean: Homepage: https://leanprover.github.io/ Source: https:... | Hacker News

Hacker Newsnew | past | comments | ask | show | jobs | submit

		peter_d_sherman on Jan 20, 2023 \| parent \| context \| favorite \| on: Idris: A language for type-driven development Some quick info for Lean: Homepage: https://leanprover.github.io/ Source: https://github.com/leanprover/lean4 Wikipedia: https://en.wikipedia.org/wiki/Lean_(proof_assistant)

agentultra on Jan 20, 2023 [–]

I also wrote a guide: https://agentultra.github.io/lean-4-hackers/

still_grokking on Jan 21, 2023 | [–]

LEAN's syntax looks really great. I wish Scala could take some inspiration.

Scala's syntax is anyway quite similar already, but would need proper Unicode support and some other "tuning" like the `:=` and the `let monadic ← effect` syntax, imho.

Consider applying for YC's Fall 2025 batch! Applications are open till Aug 4
Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact