2007/11/09

Analysis

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

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

Labels:

posted by Josh Ko @ 1:10 pm   4 項意見

Anonymous Anonymous 在 11/09/2007 5:31 pm 說：

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

 
Blogger Josh Ko 在 11/09/2007 11:20 pm 說：

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

 
Blogger Unknown 在 11/18/2008 2:10 pm 說：

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

 
Blogger Josh Ko 在 11/18/2008 2:17 pm 說：

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

 

<< 回到主頁