Zulip Chat Archive
Stream: lean4
Topic: Some idea about syntax
Minghao Liu (Jan 17 2021 at 17:21):
Very impressed by Lean4! I wrote some idea about syntax, not sure if it is appropriate to post it here... https://molikto.github.io/posts/2021-01-17.html#syntax
Huỳnh Trần Khanh (Jan 18 2021 at 00:00):
"eligibility issues" -> "legibility issues"
Huỳnh Trần Khanh (Jan 18 2021 at 00:02):
That typo sticks out to me like a sore thumb, haha.
Last updated: Dec 20 2023 at 11:08 UTC