## Stream: lean4

### Topic: Lean4 package/code discovery

#### Andrew Kent (Jan 12 2021 at 19:30):

How do people (plan to?) answer the question "is X already implemented by someone in Lean4"? (I know I may be asking this a bit prematurely, but figured why the hell not =)

In my particular case, I'm tempted to start building a package for declarative command line argument parsing (perhaps like Rust's clap or Haskell's optparse-applicative)... but it would be nice to know if someone else has started down this path already just in case =)

#### Sebastian Ullrich (Jan 14 2021 at 18:06):

It's probably a bit early to invest time in building a leanpkg index or anything similarly fancy :) , but it would be great to have something like https://leanprover-community.github.io/lean_projects.html for Lean 4 projects!

#### Bryan Gin-ge Chen (Jan 14 2021 at 18:58):

If everyone tags their Lean 4 repos with lean4 on GitHub, we would get a crude directory here: https://github.com/topics/lean4

Last updated: May 18 2021 at 22:15 UTC