Lean from prelude

Stream: new members

[Grigoriy Prokhrov]

Did someone implemented simple lean library from scratch for educational purposes starting from prelude statement?

[Bulhwi Cha]

I tried and failed last year. I'm no longer interested in trying it again.