このAgdaのエラーとは？

Question

私が初めてAgdaをしようとしていると私はBoolデータ型を定義した、すべてのチュートリアルのような基本的な機能は言う：私はこれをロードしようとすると

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

それはより多くの「理由は動揺を取得1つのマッチするタイプの署名が「真でない」と判断し、「真ではない」を赤でハイライトする。私は間違って何をしていますか？

Answer 1

Boolのデータコンストラクタをインデントする必要があります。