Agda: Function Parsing error

1
votes

I'm new to agda, and following a simple example in the book little MLer. Could anyone help me to figure out why the compiler gives me a parsing error?

Thank you

data Shish (a : Set) : Set where
  Bottom : a → Shish a
  Onion : Shish a → Shish a
  Lamb : Shish a → Shish a
  Tomato : Shish a → Shish a

data Rod : Set where
  Dagger : Rod
  Fork : Rod
  Sword : Rod

data Plate : Set where
  Gold-plate : Plate
  Silver-plate : Plate
  Brass-plate : Plate

what_bottom : Shish (a : Set) → Bool
what_bottom (Bottom x) → x
what_bottom (Onion x) → what_bottom x
what_bottom (Lamb x) → what_bottom x
what_bottom (Tomato x) → what_bottom x



/Volumes/Little/mko_io/cat/tmp/mler.agda:54,24-24
        /Volumes/Little/mko_io/cat/tmp/mler.agda:54,24: Parse error
        :<ERROR>
         Set) → Bool
        what_bottom (Bott...
2
parsingagda

2 Answers

2
votes

The data type definitions are properly defined, but this is not the way one defines functions in Agda. A good starting tutorial is Dependent types at work

Functions are defined with the equal sign.

id : {A : Set} → A → A
id a = a

Moreover, the dependent type must be declared before like so either implicitly or explicitly.

what_bottom : {A : Set} → Shish A → ...

Lastly, that function cannot be defined with a return type Bool. It can have type a though.

0
votes

As an additional syntactic point, in Agda, underscores are placeholders for mixfix arguments: what_bottom is a mixfix name with one parameter between what and bottom. So you'll end up with a function that you'd use as what (Onion $ Lamb $ Bottom) bottom which is probably not what you intended. Just call it whatBottom or what‿bottom if you're feeling extra.