Lean #04
https://lambda-kansai.connpass.com/event/370114/
3.1.8 練習問題から
usabarashi.icon sorry の使い所が Scala の ??? に近い
usabarashi.icon Pyton だとNotImplementedError
takezaki.icon Kotlin だと TODO() がある https://kotlinlang.org/api/core/kotlin-stdlib/kotlin/-t-o-d-o.html
3.2.3 から読む
Loogle
Lean Explore
#errata Lean Explorer じゃなくて Lean Explore
kakkun61.icon 読書を名前順下から始めると、今度はまん中の人が毎回読むことになりそう 誰までいったかメモした方がいいのかしら 自分が気にしすぎ?
takezaki.icon 個人的にはあんまり気にならないですが、一度全員の意思を確認しておいてもいいかも
ebi_chan.icon 関係ないけど、国語の授業で音読する時を思い出しますね
takezaki.icon 今日は何日だから何番目の hoge さん、みたいにします?w
ebi_chan.icon 均等であることにこだわりすぎると学校の授業みたいになって個人的には嫌なんですよねw
takezaki.icon 同意です。しかし「takezaki.iconがやりたいから全部やります」みたいになってもなぁ 🍵
ebi_chan.icon 「読み上げたい人」を決めておいてその人たちで回す?
takezaki.icon 賛成(次回からお試しでいいかも)
ebi_chan.icon やってみます。connpassで枠を分けた上で、次回の初めに説明して読み上げ役を決めます
kakkun61.icon 存在量化、全称量化の章節も手を動かしてみないと分かった実感がないなー
usabarashi.icon tab を押すと勝手に証明が補完されてしまう。。。ので練習にならない。。。
ebi_chan.icon それは練習問題やる時に困りますね
https://ive.lean-lang.org/ はWeb上で使える補完機能のないVS Codeなのでいいかも
takezaki.icon 単に copilot などの支援機能をオフでもいいかも
メモ
一般の二項関係と反射律・対称律・推移律の話は知っておくといいかも
https://mathlandscape.com/binary-relation/
宿題
3.3.4 練習問題
次は Lean #05