leanprover-community / lean4game

Server to host lean games.
https://adam.math.hhu.de
GNU General Public License v3.0
197 stars 35 forks source link

feat: Generate a structure of Korean document #260

Closed 0417taehyun closed 2 months ago

0417taehyun commented 2 months ago

What I've done

FYI

There are some people interested in Lean and build a community to contribute this game in Korean. We are going to contribute the details later hence I just created the structure of it through config.json.

joneugster commented 2 months ago

Thanks!