Zulip Chat Archive

Stream: new members

Topic: Beginner question


view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Jan 11 2021 at 17:37):

I'm missing the error message

view this post on Zulip Kevin Buzzard (Jan 11 2021 at 17:37):

And you're probably missing open term

view this post on Zulip 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

view this post on Zulip Reid Barton (Jan 11 2021 at 17:43):

Same reason that

def size : term -> 
| anything := 1

doesn't error

view this post on Zulip Guilherme Espada (Jan 11 2021 at 18:00):

Thanks!


Last updated: May 11 2021 at 14:11 UTC