我玩了半個早上的 Cytus II
用來做筆記跟看電子課本
剛剛又玩五首 Cytus II
結果一退出 電量100%
我看不懂台灣的交通…
每次過路都覺得會被撞倒
/w\
尤其在行人過路的時候
我永遠不明白為什麼有車會駛過來…
只視乎你如何人手分配哪台 VM 在哪台實體機上而已
Ceph 的話會自動在十台的儲存裏自動分配東西要擺哪裡
然後因為你有設定 replicated 備援所以東西都會複製兩份（或是三份）
接著網管會來投訴交換機效能被你們的 Ceph 都吞了（#
於是強者不進線上討論區，線上討論區就更多智障，強者就更不願意進去
A functor that maps a category to itself
同一個pattern重複好幾次雖然看起來是loop但是實際上卻是慢慢在解決問題的概念吧
只是閱讀速度會比較慢而已不是嗎，因為還要去查那些詞的意義
這跟教授丟paper給你 叫你看完再來討論是一樣的啊
台灣通常這類東西不學英文，那種Mapiing是不存在的
你分級是指對特定領域的知識理解的程度來劃分幾個等級的概念？
有些時候是會使用 Google 但是看不懂裡面的資料
這就是為啥 github issue board 跟 mailing list 存在
就像 1 + 1 = 2 明明很初階，卻可以變成一個很大的問題
就算看不懂，也能建立一些共識吧
有共識就有討論的可能性，大概(
forall x. forall y. forall z. (x=y) and (y=z) -> x=z
forall x. forall y. forall z. (x=y) and (y=z) -> x=z
我大腦並沒有用纜線跟你連接起來，並不知道那些符號對你而言是啥
我大腦並沒有用纜線跟你連接起來，並不知道那些符號對你而言是啥
為什麼會被切開？
因為強的人只和強的討論？
所以較低階的問題就被無視了？
為什麼會被切開？
因為強的人只和強的討論？
所以較低階的問題就被無視了？
= 這個符號在我們目前的討論範圍中 需要先定義一次
啊為什麼你不能把你解數學的邏輯用到一般的討論上XD
啊為什麼你不能把你解數學的邏輯用到一般的討論上XD
錯誤: 數學 not defined
錯誤: 邏輯 not defined
錯誤: 一般 not defined
錯誤: 討論 not defined
錯誤: 數學 not defined
錯誤: 邏輯 not defined
錯誤: 一般 not defined
錯誤: 討論 not defined
就 因為我們等一下的討論會需要 = 這個符號的精確定義
好我懂了，但是目前的教育制度是以所有領域的綜合分數去做區分的吧？
那如果有人其中某個領域特別強時該怎麼辦？
好我懂了，但是目前的教育制度是以所有領域的綜合分數去做區分的吧？
那如果有人其中某個領域特別強時該怎麼辦？
/home/daisuke/secretplace/video/*
如果你要放 seadog video
你是要 /home/daisuke/video/seadog007
還是 /home/daisuke/seadog007/video
?
所以去 Mail 撈一下，至少 Mail 是正常ㄉ
沒有 我只是好奇 seadog 有沒有多到需要當成一個類別
然後剛剛那三條是讓 「=」 這個符號符合等價關係的要求
第一條說的是「不相交」這個定律
對於所有x 來說 (suc x = zero) 這條不會成立
所以
1 就是 suc zero
2 就是 suc ( suc zero)
0 + y = 0
(suc x) + y = suc ( x + y)
這兩條配合剛剛定義的東西就可以拿來運算所有自然數的加法ㄌ
經過一番完全沒有深思熟慮的臨時起意我決定要來學rust
他的意思是
對於所有的公式φ
把 φ 當中的 v 代換0 會成立的話
且
(如果 φ 成立 ，把φ當中的v代換成 suc v 也會成立) 會成立的話
則
對於所有的 v, φ 都成立
然後我們可以證明 在 n 成立時, n+1 也會成立
好反正我們剛剛用邏輯系統把整個自然數ㄉ公理定義完ㄌ
HA ├ suc zero + suc zero = suc (suc zero)
HA├ suc zero + suc zero = suc (zero + suc zero) 且 suc (zero + suc zero) = suc (suc zero) -> suc zero + suc zero = suc (suc zero)
HA ├ suc zero + suc zero = suc (zero + suc zero) 且 suc (zero + suc zero) = suc (suc zero)