2007/11/09

Analysis

想試著用 Agda 寫實數,可是寫不出來 ─ 光要證明無窮項的有理數列遞增有上界就超麻煩 XD。

--
反正寫這個兩邊的人都不想看 XD。

Labels:

Anonymous scm11/09/2007 5:31 pm 說:

Data.Real 之中有一個實數的 implementation. 這跟你想要的一樣嗎?

 
Blogger Josh Ko11/09/2007 11:20 pm 說:

雖然形式和我想的不太一樣,不過好像是耶!要再研究一下 XD。

 
Blogger XOO11/18/2008 2:10 pm 說:

唔?現在 agda 裡面已經沒看到這個 module,是發生什麼事情,還是擺在別的地方?

 
Blogger Josh Ko11/18/2008 2:17 pm 說:

這指的是舊的 library,現在在 Agda/examples/lib/ 下面。

 

<< 回到主頁