## Stream: general

### Topic: equation compiler surprisingly liberal

#### Kevin Buzzard (Oct 10 2019 at 07:38):

inductive mytype
| T : mytype
| F : mytype

namespace mytype

def f : mytype → ℕ
| T := 34
| cake := 19


If I asked you to guess whether the definition of f compiled, what would you say?

#eval f T -- 34
#eval f F  -- 19


Works fine.

#### Johan Commelin (Oct 10 2019 at 07:39):

How about #eval f cake?

#### Sebastian Ullrich (Oct 10 2019 at 07:40):

I'm not sure why you would expect a different result. T is a constructor pattern, while cake is an (irrefutable) variable pattern.

#### Johan Commelin (Oct 10 2019 at 07:41):

Lean let's you have your cake and eat it too

#### Sebastian Ullrich (Oct 10 2019 at 07:41):

At least until it supports linear cake types

#### Johan Commelin (Oct 10 2019 at 07:42):

Lean: dependent cakes all the way down

#### Kevin Buzzard (Oct 10 2019 at 07:52):

I'm not sure why you would expect a different result. T is a constructor pattern, while cake is an (irrefutable) variable pattern.

penny drops

#### Kevin Buzzard (Oct 10 2019 at 07:53):

Yeah, sorry, I get it now. Expected behaviour :D

Last updated: May 17 2021 at 22:15 UTC