这是什么 Agda 错误？

Question

我是第一次尝试 Agda，我已经定义了 Bool 数据类型及其基本功能，就像所有教程所说的那样：

data Bool : Set where
true : Bool
false : Bool 
not : Bool -> Bool
not true = false
not false = true
etc...

当我尝试加载它时，它会感到不安，因为“左侧的多个匹配类型签名不正确”并且它以红色突出显示“不正确”。我做错了什么？

Answer 1

你需要缩进Bool的数据构造函数。