Zulip Chat Archive

Stream: lean4

Topic: parens on method LHS


view this post on Zulip Reid Barton (Jan 28 2021 at 14:26):

Is it intended that this program compiles?

class C (α : Type) where
  op : α  α  α

instance : C Nat where
  op (a b) := a + b    -- should be `op a b := a + b`

view this post on Zulip Sebastian Ullrich (Jan 28 2021 at 14:26):

I think so, it's no different from def op (a b) := a + b

view this post on Zulip Reid Barton (Jan 28 2021 at 14:27):

It can lead to bewildering error messages if one tries to write something like

inductive X
| mk : Nat  X

instance : C X where
  op (X.mk a) (X.mk b) := X.mk (a + b)    -- function of 4 variables?

view this post on Zulip Sebastian Ullrich (Jan 28 2021 at 14:27):

That is, it's a group of binders without type

view this post on Zulip Reid Barton (Jan 28 2021 at 14:28):

hmm, I see

view this post on Zulip Reid Barton (Jan 28 2021 at 14:28):

I'm not very good at predicting what Lean 4 will understand yet

view this post on Zulip Kevin Buzzard (Jan 28 2021 at 14:28):

I don't see! How does op (a b) even parse?

view this post on Zulip Reid Barton (Jan 28 2021 at 14:29):

Well this whole where ... construction is new

view this post on Zulip Sebastian Ullrich (Jan 28 2021 at 14:31):

Think of it as def op (a b : _), aka def op (a : _) (b : _)

view this post on Zulip Sebastian Ullrich (Jan 28 2021 at 14:41):

@Reid Barton I think the rule here is that op is a signature and we do not support direct pattern matching in signatures. But certainly we shouldn't accept X.mk as a binder name. If it had errored with "expected atomic identifier", do you think that would have led you to the right path?

view this post on Zulip Reid Barton (Jan 28 2021 at 14:41):

That should probably be an error in any case, yeah

view this post on Zulip Reid Barton (Jan 28 2021 at 14:41):

I didn't really expect putting a pattern there to work, but then I got confused when it sort-of worked instead

view this post on Zulip Mario Carneiro (Jan 28 2021 at 15:01):

Why can't patterns go there? That's how it would work in haskell

view this post on Zulip Mario Carneiro (Jan 28 2021 at 15:01):

how do you write an equation compiler definition in a where clause?

view this post on Zulip Sebastian Ullrich (Jan 28 2021 at 15:04):

It's a signature, so name binders | equations

view this post on Zulip Mario Carneiro (Jan 28 2021 at 15:07):

So:

inductive X
| mk : Nat  X

instance : C X where
  op : X -> X -> X
  | (X.mk a) (X.mk b) := X.mk (a + b)

?

view this post on Zulip Mario Carneiro (Jan 28 2021 at 15:07):

or are there supposed to be commas now

view this post on Zulip Mario Carneiro (Jan 28 2021 at 15:08):

Is the type ascription optional?

view this post on Zulip Sebastian Ullrich (Jan 28 2021 at 17:16):

Yes to both

instance : C X where
  op
  | X.mk a, X.mk b => X.mk (a + b)

Last updated: May 18 2021 at 23:14 UTC