agda - 这个 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 的数据构造函数。