DEERTOPIAVISIBILITY	public

2026-02-10

This section is empty…

korean lean 4 conversation

ID	af0301a7-a2cf-416e-ac4e-ffe4c08d8962
DEERTOPIAVISIBILITY	public

from the korean haskell discord server, discussing lean 4

unimplemented! (verse-block)

{:type "verse-block", :affiliated {}, :contents-begin 426, :contents-end 870, :position {:start {:line 15, :column 1, :offset 412}, :end {:line 24, :column 1, :offset 882}}, :children ([:b ("차불휘")] ": 방금 제가 메타매스 원의 고급 기능을 튜토리얼 영상에서 대충 맛봤는데, 그 내용이 이해가 거의 안 가더군요.\n" [:b ("차불휘")] ": 여러분은 증명 보조기의 메타프로그래밍 기능은 언제 배우셨나요?\n" [:b ("차불휘")] ": " [:span.org-link.external [:a {:href "https://github.com/leanprover-community/lean4-metaprogramming-book"} "https://github.com/leanprover-community/lean4-metaprogramming-book"]] "\n" [:b ("차불휘")] ": 저는 아직 이 교재를 안 봤어요\n" [:b ("녀뉴뇨뉴")] ": Lean 메타프로그래밍은 지금 공부하는중인데, 모나드 사용에 좀 익숙해질 필요가 있고 " [:b ("파싱관련한")] " 기초적인 내용은 기본적으로 아셔야 할것같습니다.\n" [:b ("차불휘")] ": 그러면 어차피 언젠가 저도 배워야 하는 모나드와 파싱을 알아야겠군요. 감사합니다!\n" [:b ("차불휘")] ": 늘 그렇듯이, 지금 제가 뭐부터 배울지 정하느라 어떤 건 순위가 좀 밀려나기도 해요. 그렇지만 슬슬 제가 저 내용들도 배울 때가 가까워지고 있어요. \n")}

unimplemented! (verse-block)

{:type "verse-block", :affiliated {}, :contents-begin 897, :contents-end 1494, :position {:start {:line 25, :column 1, :offset 883}, :end {:line 34, :column 1, :offset 1506}}, :children ([:b ("차불휘")] ": 방금 제가 메타매스 원의 고급 기능을 튜토리얼 영상에서 대충 맛봤는데, 그 내용이 이해가 거의 안 가더군요.\n" [:b ("차불휘")] ": [Addressing the room] Are there any pieces of helpfulness for learning Lean 4's metaprogramming?\n" [:b ("차불휘")] ": " [:span.org-link.external [:a {:href "https://github.com/leanprover-community/lean4-metaprogramming-book"} "https://github.com/leanprover-community/lean4-metaprogramming-book"]] "\n" [:b ("차불휘")] ": I've already seen this resource\n" [:b ("녀뉴뇨뉴")] ": I'm studying Lean metaprogramming now. There is a need to get used to working in monads, and you have to understand the basics of [Lean 4's] parsing internals.\n" [:b ("차불휘")] ": 그러면 어차피 언젠가 저도 배워야 하는 모나드와 파싱을 알아야겠군요. 감사합니다!\n" [:b ("차불휘")] ": 늘 그렇듯이, 지금 제가 뭐부터 배울지 정하느라 어떤 건 순위가 좀 밀려나기도 해요. 그렇지만 슬슬 제가 저 내용들도 배울 때가 가까워지고 있어요. \n")}