这是什么Agda错误？

Question

我尝试阿格达的第一时间，我已经定义了Bool数据类型和它像所有的教程基本功能说：

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

当我尝试加载这一点，得到不高兴，因为“多比左手边的一个匹配类型签名不是真实的“，并以红色突出显示”不正确“。我究竟做错了什么？

Answer 1

您需要缩进数据构造函数Bool。