What is this Agda error?

Question

I'm trying out Agda for the first time and I've defined the Bool data type and its basic functions like all the tutorials say:

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

When I try to load this it gets upset because "more than one matching type signature for left hand side not true" and it highlights "not true" in red. What am I doing wrong?

Answer 1

You need to indent the data constructors of Bool.