Zulip Chat Archive

Stream: new members

Topic: Beginner question


Guilherme Espada (Jan 11 2021 at 17:29):

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 (Jan 11 2021 at 17:37):

I'm missing the error message

Kevin Buzzard (Jan 11 2021 at 17:37):

And you're probably missing open term

Guilherme Espada (Jan 11 2021 at 17:41):

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 (Jan 11 2021 at 17:43):

Same reason that

def size : term -> 
| anything := 1

doesn't error

Guilherme Espada (Jan 11 2021 at 18:00):

Thanks!


Last updated: Dec 20 2023 at 11:08 UTC