Zulip Chat Archive

Stream: general

Topic: equation compiler surprisingly liberal


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

view this post on Zulip Johan Commelin (Oct 10 2019 at 07:39):

How about #eval f cake?

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

view this post on Zulip Johan Commelin (Oct 10 2019 at 07:41):

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

view this post on Zulip Sebastian Ullrich (Oct 10 2019 at 07:41):

At least until it supports linear cake types

view this post on Zulip Johan Commelin (Oct 10 2019 at 07:42):

Lean: dependent cakes all the way down

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

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