Zulip Chat Archive

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: Dec 20 2023 at 11:08 UTC