agda - 模塊縮進

  显示原文与译文双语对照的内容

閱讀文檔時,我覺得模塊內部的定義應該縮進。 但是,當瀏覽標準庫或者文件時,人們似乎沒有縮進他們的模塊,至少不是"主要"模塊。

具體來說,當我寫文件" foo.agda"時,我應該做


module Foo where
 a :.. .
 a =.. .

或者


module Foo where
a :.. .
a =.. .

时间: 原作者:

是,Agda通過縮進確定屬於某個模塊的內容。 但是,( 唯一) 頂級模塊是一個例外- 什麼是不明確的,它是整個文件 !

這意味著你可以使用兩種樣式。 我個人沒有縮進,它比stdlib風格更容易閱讀和一致。

原作者:
...