Bound View

最近受到 view 的啟發(?)，做了幾個簡單但是還滿有趣的東西，例如可以把 N 拆成某個數字以上跟以下，然後對他作 pattern matching，傳統上會用 if … then … else 不過寫起來到是挺有趣的

data Bound (k : ℕ) : ℕ → Set where
below : (n : ℕ) → (l : ℕ) → (l + n ≡ k) → Bound k n
above : (n : ℕ) → (l : ℕ) → (k + (suc l) ≡ n) → Bound k n

快瘋了

想證明 pop 跟 push 對於 queue 的操作而言, 會保持等式, 也就是 (即 ), 而對於同樣的 queue, pop 跟 push 必須產生同樣的結果, 而不管用什麼樣的表示。

但光是把 case split 出來, 就一堆東西了, 到底要怎麼寫啊, 不是這樣的吧 囧

用 C++ Template 建表

（兩年前寫的東西，當時寫在 bbs 上沒公開，最近有空稍微整理一下。）

C++ TMP 可以利用 compile-time 計算一些東西, 凡是 static 資訊都可以算出來, 但如果要 runtime 到才存取呢？想了一個下午, 比較接近的方式是在 class template 裡頭放個 static array,  並且呼叫 value<N>::result 將資料填入表內。

用 Visual C++ Express 編譯 Qt4/Win Open Source Edititon

Update 01/30/09:　目前最新版的 Qt4 已經直接支援不需要 patch 囉。滿久的事情 …

Qt4 Open Source Edition 本身在 Windows 下並不支援用 gcc 以外的編譯器編譯, 不過經由非官方的 patch, 可以支援 Visual Studio (express), 簡單講解一下步驟。
本說明參考：

http://wiki.qtcentre.org/index.php?title=Qt4_with_Visual_Studio
http://kjellkod.blogspot.com/2007/02/qt4-on-free-ide-visual-studio-express.html
習慣看英文的就直接看這篇。