Weird errors when working on DFA.lean

Stream: CSLib

[Ching-Tsun Chou]

Never mind. I figured out what's going on: I should have written:

variable {State : Type _} {Symbol : Type _}

[Chris Henson]

Can you clarify what the difference is? This thread is more useful with the original context.

[Ching-Tsun Chou]

I was using (...) instead of {...}.

[Ching-Tsun Chou]

A very silly mistake.