Beginner question

Stream: new members

[Guilherme Espada]

The following code:

inductive term
|t_true : term
|t_false : term
|t_zero : term


def size : term -> ℕ
| t_true := 1
| t_false := 1
| t_zero := 1

does not work. What am I missing?

[Kevin Buzzard]

I'm missing the error message

[Kevin Buzzard]

And you're probably missing open term

[Guilherme Espada]

This fixes it!
(the error message is invalid application, function expected)
Another question, when I list only a single option on the size function, it doesn't error. Why?

def size : term -> ℕ
| t_true := 1

[Reid Barton]

Same reason that

def size : term -> ℕ
| anything := 1

doesn't error

[Guilherme Espada]

Thanks!