agda - 模块缩进

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

阅读文档时,我觉得模块内部的定义应该缩进。 但是,当浏览标准库或者文件时,人们似乎没有缩进他们的模块,至少不是"主要"模块。

具体来说,当我写文件" foo.agda"时,我应该做


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

或者


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

时间: 原作者:

0 0

是,Agda通过缩进确定属于某个模块的内容。 但是,( 唯一) 顶级模块是一个例外- 什么是不明确的,它是整个文件 !

这意味着你可以使用两种样式。 我个人没有缩进,它比stdlib风格更容易阅读和一致。

原作者:
...